src/Pure/Isar/parse_spec.ML
changeset 63285 e9c777bfd78c
parent 63183 4d04e14d7ab8
child 63352 4eaf35781b23
--- a/src/Pure/Isar/parse_spec.ML	Sat Jun 11 13:57:59 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Sat Jun 11 16:41:11 2016 +0200
@@ -67,7 +67,7 @@
 
 val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs;
 
-val specification = Parse.fixes -- where_multi_specs;
+val specification = Parse.vars -- where_multi_specs;
 
 
 (* basic constant specifications *)
@@ -157,7 +157,7 @@
 
 val obtain_case =
   Parse.parbinding --
-    (Scan.optional (Parse.and_list1 Parse.fixes --| Parse.where_ >> flat) [] --
+    (Scan.optional (Parse.and_list1 Parse.vars --| Parse.where_ >> flat) [] --
       (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
 
 val obtains = Parse.enum1 "|" obtain_case;