
diff -r 4e4738698db4 -r 9f394a16c557 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Pure.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -280,7 +280,7 @@
 
 val trans_pat =
   Scan.optional
-    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
+    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.name --| @{keyword ")"})) "logic"
     -- Parse.inner_syntax Parse.string;
 
 fun trans_arrow toks =
@@ -403,7 +403,7 @@
 
 val _ =
   Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
-    (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
+    (Parse.and_list1 Parse.thms1 -- Parse.for_fixes
       >> (fn (facts, fixes) =>
           #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
 
@@ -442,7 +442,7 @@
 
 val _ =
   hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
-    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
+    (Parse.position Parse.name) (Global_Theory.check_fact o Proof_Context.theory_of);
 
 in end\<close>
 
@@ -454,18 +454,18 @@
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
-    ((Parse.binding --| @{keyword "="}) -- Parse.xthms1 -- Parse.for_fixes
+    ((Parse.binding --| @{keyword "="}) -- Parse.thms1 -- Parse.for_fixes
       >> (uncurry Bundle.bundle_cmd));
 
 val _ =
   Outer_Syntax.command @{command_keyword include}
     "include declarations from bundle in proof body"
-    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
+    (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd));
 
 val _ =
   Outer_Syntax.command @{command_keyword including}
     "include declarations from bundle in goal refinement"
-    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
+    (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.including_cmd));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_bundles}
@@ -484,7 +484,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword context} "begin local theory context"
-    ((Parse.position Parse.xname >> (fn name =>
+    ((Parse.position Parse.name >> (fn name =>
         Toplevel.begin_local_theory true (Named_Target.begin name)) ||
       Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
         >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
@@ -550,7 +550,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword sublocale}
     "prove sublocale relation between a locale and a locale expression"
-    ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
+    ((Parse.position Parse.name --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
       interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) =>
         Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations)))
     || interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
@@ -684,7 +684,7 @@
 ML \<open>
 local
 
-val facts = Parse.and_list1 Parse.xthms1;
+val facts = Parse.and_list1 Parse.thms1;
 
 val _ =
   Outer_Syntax.command @{command_keyword then} "forward chaining"
@@ -773,9 +773,9 @@
   Outer_Syntax.command @{command_keyword case} "invoke local context"
     (Parse_Spec.opt_thm_name ":" --
       (@{keyword "("} |--
-        Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
+        Parse.!!! (Parse.position Parse.name -- Scan.repeat (Parse.maybe Parse.binding)
           --| @{keyword ")"}) ||
-        Parse.position Parse.xname >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
+        Parse.position Parse.name >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
 
 in end\<close>
 
@@ -906,7 +906,7 @@
 local
 
 val calculation_args =
-  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
+  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.thms1 --| @{keyword ")"})));
 
 val _ =
   Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
@@ -956,7 +956,7 @@
 local
 
 val opt_modes =
-  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
 
 val _ =
   Outer_Syntax.command @{command_keyword help}
@@ -1025,13 +1025,13 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_locale}
     "print locale of this theory"
-    (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
+    (Parse.opt_bang -- Parse.position Parse.name >> (fn (b, name) =>
       Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_interps}
     "print interpretations of locale for this theory or proof context"
-    (Parse.position Parse.xname >> (fn name =>
+    (Parse.position Parse.name >> (fn name =>
       Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
 
 val _ =
@@ -1100,19 +1100,19 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_statement}
     "print theorems as long statements"
-    (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
+    (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts);
 
 val _ =
   Outer_Syntax.command @{command_keyword thm} "print theorems"
-    (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
+    (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms);
 
 val _ =
   Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
-    (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
+    (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false);
 
 val _ =
   Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
-    (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
+    (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true);
 
 val _ =
   Outer_Syntax.command @{command_keyword prop} "read and print proposition"
@@ -1156,8 +1156,8 @@
 local
 
 val theory_bounds =
-  Parse.position Parse.theory_xname >> single ||
-  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
+  Parse.position Parse.theory_name >> single ||
+  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_name) --| @{keyword ")"});
 
 val _ =
   Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
@@ -1177,14 +1177,14 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
-    (Parse.xthms1 >> (fn args =>
+    (Parse.thms1 >> (fn args =>
       Toplevel.keep (fn st =>
         Thm_Deps.thm_deps (Toplevel.theory_of st)
           (Attrib.eval_thms (Toplevel.context_of st) args))));
 
 
 val thy_names =
-  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
+  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name));
 
 val _ =
   Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
@@ -1260,7 +1260,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword realizers}
     "specify realizers for primitive axioms / theorems, together with correctness proof"
-    (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
+    (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
      (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
        (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
 
@@ -1276,7 +1276,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
-    (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
+    (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
       Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
 
 in end\<close>




