repaired rail diagram (cf. 8450b944e58a);
authorwenzelm
Wed, 22 Oct 2014 11:24:48 +0200
changeset 58761 b5ecbb1c4dc5
parent 58760 3600ee38daa0
child 58762 4fedc5d4b2fe
repaired rail diagram (cf. 8450b944e58a);
src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue Oct 21 22:18:06 2014 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Oct 22 11:24:48 2014 +0200
@@ -331,11 +331,10 @@
 
   @{rail \<open>
     @{syntax_def mixfix}: '('
-      @{syntax template} prios? @{syntax nat}? |
-      (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
-      @'binder' @{syntax template} prios? @{syntax nat} |
-      @'structure'
-    ')'
+      (@{syntax template} prios? @{syntax nat}? |
+        (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
+        @'binder' @{syntax template} prios? @{syntax nat} |
+        @'structure') ')'
     ;
     template: string
     ;