src/Doc/IsarRef/Inner_Syntax.thy

   Isabelle mixfix syntax is inspired by {\OBJ} \cite{OBJ}.  It allows
   to specify any context-free priority grammar, which is more general
   than the fixity declarations of ML and Prolog.
 
   @{rail "
-    @{syntax_def mixfix}: '(' mfix ')'
-    ;
-    @{syntax_def struct_mixfix}: '(' ( mfix | @'structure' ) ')'
-    ;
-
-    mfix: @{syntax template} prios? @{syntax nat}? |
+    @{syntax_def mixfix}: '('
+      @{syntax template} prios? @{syntax nat}? |
       (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
-      @'binder' @{syntax template} prios? @{syntax nat}
+      @'binder' @{syntax template} prios? @{syntax nat} |
+      @'structure'
+    ')'
     ;
     template: string
     ;
     prios: '[' (@{syntax nat} + ',') ']'
   "}
 
   The string given as @{text template} may include literal text,
   spacing, blocks, and arguments (denoted by ``@{text _}''); the
   special symbol ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'')
-  represents an index argument that specifies an implicit structure
-  reference (see also \secref{sec:locale}).  Infix and binder
-  declarations provide common abbreviations for particular mixfix
+  represents an index argument that specifies an implicit
+  @{text "\<STRUCTURE>"} reference (see also \secref{sec:locale}).  Infix and
+  binder declarations provide common abbreviations for particular mixfix
   declarations.  So in practice, mixfix templates mostly degenerate to
   literal text for concrete syntax, such as ``@{verbatim "++"}'' for
   an infix symbol.
 *}
 

   @{rail "
     (@@{command type_notation} | @@{command no_type_notation}) @{syntax target}?
       @{syntax mode}? \\ (@{syntax nameref} @{syntax mixfix} + @'and')
     ;
     (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \\
-      (@{syntax nameref} @{syntax struct_mixfix} + @'and')
+      (@{syntax nameref} @{syntax mixfix} + @'and')
     ;
-    @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax struct_mixfix} + @'and')
+    @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
   "}
 
   \begin{description}
 
   \item @{command "type_notation"}~@{text "c (mx)"} associates mixfix