src/Pure/Isar/parse_spec.ML

     ((opt_thm_name ":" -- Parse.prop -- if_assumes -- Parse.for_fixes >> Scan.triple1) --|
       Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
 
 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 *)
 
 val constdecl =

   Parse.$$$ "when" |-- Parse.!!! statement >> pair false ||
   Scan.succeed (true, []);
 
 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;
 
 val long_statement =