--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Fri May 25 13:47:58 2018 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri May 25 21:00:47 2018 +0200
@@ -281,12 +281,14 @@
@{syntax_def mixfix}: '('
(@{syntax template} prios? @{syntax nat}? |
(@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
- @'binder' @{syntax template} prios? @{syntax nat} |
+ @'binder' @{syntax template} prio? @{syntax nat} |
@'structure') ')'
;
@{syntax template}: string
;
prios: '[' (@{syntax nat} + ',') ']'
+ ;
+ prio: '[' @{syntax nat} ']'
\<close>}
The string given as \<open>template\<close> may include literal text, spacing, blocks,