Say I have the following definition of a reflexive and transitive closure of a relation, where relations are represented by binary predicates:

```
inductive
closure :: "(['a, 'a] ⇒ bool) ⇒ (['a, 'a] ⇒ bool)"
for ℛ (infix "→" 50)
where
gen:
"x → y ⟹ closure (→) x y" |
refl:
"closure (→) x x" |
trans:
"⟦closure (→) x y; closure (→) y z⟧ ⟹ closure (→) x z"
```

I want to have a nicer syntax for applications of `closure`

. Say I’d like to be able to write `x *(→)* y`

for `closure (→) x y`

. The problem is that the argument order in this notation doesn’t match the argument order of the function `closure`

.

I thought that perhaps the use of `\<index>`

could help. Unfortunately, the documentation of `\<index>`

in the Isabelle/Isar Reference Manual is very terse, and I couldn’t really make sense of it. I played a bit with `\<index>`

but didn’t find any workable solution.

What puzzled me was that apparently `\<index>`

gets translated to `⇘some_index⇙`

, judging from some error messages I got. I tried to use `⇘ℛ⇙`

to mark the position where the base relation should go, but this didn’t work either.