# HG changeset patch
# User wenzelm
# Date 1413969888 -7200
# Node ID b5ecbb1c4dc58eb36e69fba489aaa8b765477c17
# Parent  3600ee38daa071ea8fd88c6ce84f6920b8d23bcf
repaired rail diagram (cf. 8450b944e58a);

diff -r 3600ee38daa0 -r b5ecbb1c4dc5 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
     ;