just one syntax category "mixfix" -- check structure annotation semantically;

--- a/src/Doc/IsarRef/Inner_Syntax.thy	Tue Apr 09 12:29:36 2013 +0200
+++ b/src/Doc/IsarRef/Inner_Syntax.thy	Tue Apr 09 12:56:26 2013 +0200
@@ -362,14 +362,12 @@
   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
     ;
@@ -379,9 +377,9 @@
   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.
@@ -568,9 +566,9 @@
       @{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}

--- a/src/Pure/Isar/isar_syn.ML	Tue Apr 09 12:29:36 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 09 12:56:26 2013 +0200
@@ -208,13 +208,13 @@
 val _ =
   Outer_Syntax.local_theory @{command_spec "notation"}
     "add concrete syntax for constants / fixed variables"
-    (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
       >> (fn (mode, args) => Specification.notation_cmd true mode args));
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "no_notation"}
     "delete concrete syntax for constants / fixed variables"
-    (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
       >> (fn (mode, args) => Specification.notation_cmd false mode args));
 
 
@@ -604,7 +604,7 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables"
-    (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
     >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
 
 val case_spec =

--- a/src/Pure/Isar/parse.ML	Tue Apr 09 12:29:36 2013 +0200
+++ b/src/Pure/Isar/parse.ML	Tue Apr 09 12:56:26 2013 +0200
@@ -298,6 +298,8 @@
 
 (* mixfix annotations *)
 
+local
+
 val mfix = string --
   !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
     Scan.optional nat 1000) >> (Mixfix o triple2);
@@ -305,18 +307,25 @@
 val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
 val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
 val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr);
+val strcture = $$$ "structure" >> K Structure;
 
 val binder = $$$ "binder" |--
   !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
   >> (Binder o triple2);
 
-fun annotation guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
-fun opt_annotation guard fix = Scan.optional (annotation guard fix) NoSyn;
+val mixfix_body = mfix || strcture || binder || infxl || infxr || infx;
+
+fun annotation guard body = $$$ "(" |-- guard (body --| $$$ ")");
+fun opt_annotation guard body = Scan.optional (annotation guard body) NoSyn;
+
+in
 
-val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx);
-val mixfix' = annotation I (mfix || binder || infxl || infxr || infx);
-val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx);
-val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx);
+val mixfix = annotation !!! mixfix_body;
+val mixfix' = annotation I mixfix_body;
+val opt_mixfix = opt_annotation !!! mixfix_body;
+val opt_mixfix' = opt_annotation I mixfix_body;
+
+end;
 
 
 (* fixes *)

--- a/src/Pure/Isar/parse_spec.ML	Tue Apr 09 12:29:36 2013 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Tue Apr 09 12:56:26 2013 +0200
@@ -20,7 +20,6 @@
   val constdecl: (binding * string option * mixfix) parser
   val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
   val includes: (xstring * Position.T) list parser
-  val locale_mixfix: mixfix parser
   val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
   val class_expression: string list parser
@@ -83,12 +82,8 @@
 
 val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.xname));
 
-val locale_mixfix =
-  Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
-  Parse.mixfix;
-
 val locale_fixes =
-  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
+  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
     >> (single o Parse.triple1) ||
   Parse.params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;