doc-src/IsarRef/Thy/Inner_Syntax.thy

       @{syntax string} @{syntax nat} ')'
     ;
     @{syntax_def mixfix}: @{syntax \"infix\"} | '(' @{syntax string} prios? @{syntax nat}? ')' |
     '(' @'binder' @{syntax string} prios? @{syntax nat} ')'
     ;
-    @{syntax_def structmixfix}: @{syntax mixfix} | '(' @'structure' ')'
+    @{syntax_def struct_mixfix}: @{syntax mixfix} | '(' @'structure' ')'
     ;
 
     prios: '[' (@{syntax nat} + ',') ']'
   "}
 

   @{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 structmixfix} + @'and')
-    ;
-    @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax structmixfix} + @'and')
+      (@{syntax nameref} @{syntax struct_mixfix} + @'and')
+    ;
+    @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax struct_mixfix} + @'and')
   "}
 
   \begin{description}
 
   \item @{command "type_notation"}~@{text "c (mx)"} associates mixfix