--- a/src/Pure/Isar/outer_parse.ML Sun Jun 11 21:59:24 2006 +0200
+++ b/src/Pure/Isar/outer_parse.ML Sun Jun 11 21:59:25 2006 +0200
@@ -61,8 +61,9 @@
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
@@ -269,6 +270,8 @@
and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
params >> map Syntax.no_syn) >> flat;
+val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
+
(* terms *)