--- a/src/Pure/Isar/outer_parse.ML Thu Nov 16 20:19:50 2006 +0100
+++ b/src/Pure/Isar/outer_parse.ML Fri Nov 17 02:19:51 2006 +0100
@@ -62,6 +62,7 @@
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 where_: token list -> string * 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
@@ -267,6 +268,8 @@
(* fixes *)
+val where_ = $$$ "where";
+
val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
val params = Scan.repeat1 name -- Scan.option ($$$ "::" |-- !!! typ)