src/Pure/Pure.thy

--- a/src/Pure/Pure.thy	Sat Jun 11 13:57:59 2016 +0200
+++ b/src/Pure/Pure.thy	Sat Jun 11 16:41:11 2016 +0200
@@ -359,7 +359,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
-    (Scan.optional Parse.fixes [] --
+    (Scan.optional Parse.vars [] --
       Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
       >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
 
@@ -756,7 +756,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)"
-    (Parse.fixes >> (Toplevel.proof o Proof.fix_cmd));
+    (Parse.vars >> (Toplevel.proof o Proof.fix_cmd));
 
 val _ =
   Outer_Syntax.command @{command_keyword assume} "assume propositions"
@@ -768,7 +768,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword define} "local definition (non-polymorphic)"
-    ((Parse.fixes --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
+    ((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
       >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
 
 val _ =
@@ -786,12 +786,12 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
-    (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- structured_statement
+    (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement
       >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
 
 val _ =
   Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
-    (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd));
+    (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd));
 
 val _ =
   Outer_Syntax.command @{command_keyword let} "bind text variables"