src/Pure/Isar/outer_parse.ML

   val opt_infix: token list -> mixfix * token list
   val opt_mixfix: token list -> mixfix * token list
   val opt_infix': token list -> mixfix * token list
   val opt_mixfix': token list -> mixfix * token list
   val const: token list -> (string * string * mixfix) * token list
+  val simple_fixes: token list -> (string * string option) list * token list
   val fixes: token list -> (string * string option * mixfix) list * token list
-  val simple_fixes: token list -> (string * string option) list * token list
+  val for_fixes: token list -> (string * string option * mixfix) list * token list
   val term: token list -> string * token list
   val prop: token list -> string * token list
   val propp: token list -> (string * string list) * token list
   val termp: token list -> (string * string list) * token list
   val arguments: token list -> Args.T list * token list

 
 val fixes =
   and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
     params >> map Syntax.no_syn) >> flat;
 
+val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
+
 
 (* terms *)
 
 val trm = short_ident || long_ident || sym_ident || term_var || number || string;