src/Pure/Isar/outer_parse.ML

   val verbatim: token list -> string * token list
   val sync: token list -> string * token list
   val eof: token list -> string * token list
   val not_eof: token list -> token * token list
   val opt_unit: token list -> unit * token list
+  val opt_keyword: string -> token list -> bool * token list
   val nat: token list -> int * token list
   val enum: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
   val enum1: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
   val list: (token list -> 'a * token list) -> token list -> 'a list * token list
   val list1: (token list -> 'a * token list) -> token list -> 'a list * token list

   val typ: token list -> string * token list
   val opt_infix: token list -> Syntax.mixfix * token list
   val opt_mixfix: token list -> Syntax.mixfix * token list
   val opt_infix': token list -> Syntax.mixfix * token list
   val opt_mixfix': token list -> Syntax.mixfix * token list
+  val mixfix': token list -> Syntax.mixfix * token list
   val const: token list -> (bstring * string * Syntax.mixfix) * token list
   val term: token list -> string * token list
   val prop: token list -> string * token list
   val propp: token list -> (string * (string list * string list)) * token list
   val termp: token list -> (string * string list) * token list

 
 val not_eof = Scan.one T.not_eof;
 
 val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
 
+fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
+
 
 (* enumerations *)
 
 fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- !!! scan) >> op ::;
 fun enum sep scan = enum1 sep scan || Scan.succeed [];

 val name = group "name declaration" (short_ident || sym_ident || string || number);
 val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
 
 val uname = underscore >> K None || name >> Some;
-  (* CB: underscore yields None, any other name Some with that string.
-     Used, for example, in the renaming of locale parameters.  *)
+
 
 (* sorts and arities *)
 
 val sort = group "sort" xname;
 

 
 val mixfix =
   (string -- !!! (opt_pris -- Scan.optional nat Syntax.max_pri))
   >> (Syntax.Mixfix o triple2);
 
-fun opt_fix guard fix =
-  Scan.optional ($$$ "(" |-- guard (fix --| $$$ ")")) Syntax.NoSyn;
+fun fix_decl guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
+fun opt_fix guard fix = Scan.optional (fix_decl guard fix) Syntax.NoSyn;
 
 val opt_infix = opt_fix !!! (infxl || infxr || infx);
 val opt_mixfix = opt_fix !!! (mixfix || binder || infxl || infxr || infx);
-
 val opt_infix' = opt_fix I (infxl || infxr || infx);
 val opt_mixfix' = opt_fix I (mixfix || binder || infxl || infxr || infx);
+val mixfix' = fix_decl !!! (mixfix || binder || infxl || infxr || infx);
 
 
 (* consts *)
 
 val const =