doc-src/IsarRef/Thy/Inner_Syntax.thy

   Isabelle types and terms.  Locally fixed parameters in toplevel
   theorem statements, locale specifications etc.\ also admit mixfix
   annotations.
 
   @{rail "
-    @{syntax_def mixfix}: '(' (
-      @{syntax string} prios? @{syntax nat}? |
+    @{syntax_def mixfix}: '(' mfix ')'
+    ;
+    @{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} ) ')'
-    ;
-    @{syntax_def struct_mixfix}: @{syntax mixfix} | '(' @'structure' ')'
-    ;
-
+      @'binder' @{syntax string} prios? @{syntax nat}
+    ;
     prios: '[' (@{syntax nat} + ',') ']'
   "}
 
   Here the @{syntax string} specifications refer to the actual mixfix
   template, which may include literal text, spacing, blocks, and

 
   \item @{command "write"} is similar to @{command "notation"}, but
   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.
 *}
 
 
 section {* The Pure syntax \label{sec:pure-syntax} *}