--- a/src/Pure/Isar/parse.ML Mon Mar 23 15:55:41 2015 +0100
+++ b/src/Pure/Isar/parse.ML Mon Mar 23 16:10:32 2015 +0100
@@ -91,7 +91,6 @@
val const_decl: (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
val for_fixes: (binding * string option * mixfix) list parser
val ML_source: Input.source parser
@@ -360,8 +359,6 @@
val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
>> (fn (xs, T) => map (rpair T) xs);
-val simple_fixes = and_list1 params >> flat;
-
val fixes =
and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1) ||
params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
--- a/src/Pure/Isar/parse_spec.ML Mon Mar 23 15:55:41 2015 +0100
+++ b/src/Pure/Isar/parse_spec.ML Mon Mar 23 16:10:32 2015 +0100
@@ -132,8 +132,9 @@
val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
val obtain_case =
- Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
- (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
+ Parse.parbinding --
+ (Scan.optional (Parse.and_list1 Parse.params --| Parse.where_ >> flat) [] --
+ (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
val general_statement =
statement >> (fn x => ([], Element.Shows x)) ||