# HG changeset patch
# User wenzelm
# Date 1527274847 -7200
# Node ID ddeb6847451a06476f217edaf8d8c46c1a4ec54a
# Parent  77f6fa78b6e1610a03afeba9ce66cbade8166b80
more accurate diagram;

diff -r 77f6fa78b6e1 -r ddeb6847451a src/Doc/Isar_Ref/Inner_Syntax.thy
--- 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,