--- a/src/Pure/Isar/outer_parse.ML Sat Mar 07 21:18:37 2009 +0100
+++ b/src/Pure/Isar/outer_parse.ML Sat Mar 07 21:19:24 2009 +0100
@@ -81,6 +81,7 @@
val opt_mixfix': mixfix parser
val where_: string parser
val const: (string * string * mixfix) parser
+ val const_binding: (binding * string * mixfix) parser
val params: (binding * string option) list parser
val simple_fixes: (binding * string option) list parser
val fixes: (binding * string option * mixfix) list parser
@@ -291,6 +292,7 @@
val where_ = $$$ "where";
val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
+val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
>> (fn (xs, T) => map (rpair T) xs);