diff -r 8a2c5dc0b00e -r d0199d9f9c5b doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Feb 04 15:56:49 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Feb 04 16:08:19 2012 +0100
@@ -339,14 +339,15 @@
   annotations.
 
   @{rail "
-    @{syntax_def mixfix}: '(' (
-      @{syntax string} prios? @{syntax nat}? |
-      (@'infix' | @'infixl' | @'infixr') @{syntax string} @{syntax nat} |
-      @'binder' @{syntax string} prios? @{syntax nat} ) ')'
+    @{syntax_def mixfix}: '(' mfix ')'
     ;
-    @{syntax_def struct_mixfix}: @{syntax mixfix} | '(' @'structure' ')'
+    @{syntax_def struct_mixfix}: '(' ( mfix | @'structure' ) ')'
     ;
 
+    mfix: @{syntax string} prios? @{syntax nat}? |
+      (@'infix' | @'infixl' | @'infixr') @{syntax string} @{syntax nat} |
+      @'binder' @{syntax string} prios? @{syntax nat}
+    ;
     prios: '[' (@{syntax nat} + ',') ']'
   "}
 
@@ -496,10 +497,6 @@
   works within an Isar proof body.
 
   \end{description}
-
-  Note that the more primitive commands @{command "syntax"} and
-  @{command "no_syntax"} (\secref{sec:syn-trans}) provide raw access
-  to the syntax tables of a global theory.
 *}