--- a/src/Pure/Isar/parse_spec.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML Sun May 29 15:40:25 2016 +0200
@@ -12,7 +12,6 @@
val simple_spec: (Attrib.binding * string) parser
val simple_specs: (Attrib.binding * string list) parser
val if_assumes: string list parser
- val spec: (string list * (Attrib.binding * string)) parser
val multi_specs: Specification.multi_specs_cmd parser
val where_multi_specs: Specification.multi_specs_cmd parser
val constdecl: (binding * string option * mixfix) parser
@@ -59,8 +58,6 @@
Scan.optional (Parse.$$$ "if" |-- Parse.!!! (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat))
[];
-val spec = (opt_thm_name ":" -- Parse.prop) -- if_assumes >> swap;
-
val multi_specs =
Parse.enum1 "|"
(opt_thm_name ":" -- Parse.prop -- if_assumes --|