Isabelle: Too many precedences in mixfix annotation

I am experimenting the following example classes.pdf in Isabelle tutorial (2020), pp6. I did my best translating the PDF content into proof text, such as changing α in the PDF to 'a, adding quotes etc.

class group = monoidl +
  fixes inverse :: "'a ⇒ 'a" ("(-÷)" [1000] 999)
  assumes invl : "x ÷ ⊗ x = 𝟭"

However, the definition above still doesn't parse, with an error:

Too many precedences in mixfix annotation

I am not sure how the inverse notation should be declared. I've encountered infix notation only so far.

Can someone help explain how the fix the "mixfix" annotation in the example?

Solution

According to the Isabelle sources of the document, it is an underscore, not a hyphen:

class group = monoidl +
  fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>"    ("(_\<div>)" [1000] 999)
  assumes invl: "x\<div> \<otimes> x = \<one>"

Replacing underscores by hyphens is a feature of the document generation. Hyphen look nicer than underscore (at least in patterns).