[isabelle-dev] abbreviation (output)

[Tobias Nipkow]

abbreviation (output)
  leq_le :: "int => int => int => bool" ("_ ≤ _ < _")
where
  "a ≤ b < c == a ≤ b & b < c"

This used to work until recently, but now (parent: 55123:a389b50e6a42 tip) I get

*** Inner syntax error: unexpected end of input

It looks like the annotation ("_ ≤ _ < _") is ignored. If I remove (output) it
works again. What am I doing wrong?

Tobias