# HG changeset patch
# User wenzelm
# Date 1482060871 -3600
# Node ID 511b30aa410018e47e4c378244a0be6fe43fda77
# Parent  4719f13989df415ee9162bf619e05ae82d978424
tuned;

diff -r 4719f13989df -r 511b30aa4100 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Dec 18 12:32:20 2016 +0100
+++ b/src/Pure/Pure.thy	Sun Dec 18 12:34:31 2016 +0100
@@ -193,19 +193,19 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword oracle} "declare oracle"
-    (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
+    (Parse.range Parse.name -- (@{keyword =} |-- Parse.ML_source) >>
       (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML"
     (Parse.position Parse.name --
-        Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
+        Parse.!!! (@{keyword =} |-- Parse.ML_source -- Scan.optional Parse.text "")
       >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword method_setup} "define proof method in ML"
     (Parse.position Parse.name --
-        Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
+        Parse.!!! (@{keyword =} |-- Parse.ML_source -- Scan.optional Parse.text "")
       >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
 
 val _ =
@@ -221,7 +221,7 @@
 val _ =
   Outer_Syntax.local_theory @{command_keyword simproc_setup} "define simproc in ML"
     (Parse.position Parse.name --
-      (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) --
+      (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword =}) --
       Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c));
 
 in end\<close>
@@ -248,7 +248,7 @@
 val _ =
   Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
     (Parse.type_args -- Parse.binding --
-      (@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
+      (@{keyword =} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
       >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
 
 in end\<close>
@@ -296,9 +296,9 @@
     -- Parse.inner_syntax Parse.string;
 
 fun trans_arrow toks =
-  ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"}) >> K Syntax.Parse_Rule ||
-    (@{keyword "\<leftharpoondown>"} || @{keyword "<="}) >> K Syntax.Print_Rule ||
-    (@{keyword "\<rightleftharpoons>"} || @{keyword "=="}) >> K Syntax.Parse_Print_Rule) toks;
+  ((@{keyword \<rightharpoonup>} || @{keyword =>}) >> K Syntax.Parse_Rule ||
+    (@{keyword \<leftharpoondown>} || @{keyword <=}) >> K Syntax.Print_Rule ||
+    (@{keyword \<rightleftharpoons>} || @{keyword ==}) >> K Syntax.Parse_Print_Rule) toks;
 
 val trans_line =
   trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
@@ -505,7 +505,7 @@
 val _ =
   Outer_Syntax.maybe_begin_local_theory @{command_keyword bundle}
     "define bundle of declarations"
-    ((Parse.binding --| @{keyword "="}) -- Parse.thms1 -- Parse.for_fixes
+    ((Parse.binding --| @{keyword =}) -- Parse.thms1 -- Parse.for_fixes
       >> (uncurry Bundle.bundle_cmd))
     (Parse.binding --| Parse.begin >> Bundle.init);
 
@@ -563,13 +563,13 @@
 
 val locale_val =
   Parse_Spec.locale_expression --
-    Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
+    Scan.optional (@{keyword +} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
 
 val _ =
   Outer_Syntax.command @{command_keyword locale} "define named specification context"
     (Parse.binding --
-      Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
+      Scan.optional (@{keyword =} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           Toplevel.begin_local_theory begin
             (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
@@ -583,7 +583,7 @@
 val interpretation_args =
   Parse.!!! Parse_Spec.locale_expression --
     Scan.optional
-      (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
+      (@{keyword rewrites} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
 
 val _ =
   Outer_Syntax.command @{command_keyword interpret}
@@ -593,10 +593,10 @@
 
 val interpretation_args_with_defs =
   Parse.!!! Parse_Spec.locale_expression --
-    (Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
-      -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
+    (Scan.optional (@{keyword defines} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+      -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword =} -- Parse.term))) [] --
     Scan.optional
-      (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
+      (@{keyword rewrites} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation}
@@ -607,7 +607,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword sublocale}
     "prove sublocale relation between a locale and a locale expression"
-    ((Parse.position Parse.name --| (@{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)) =>
@@ -630,12 +630,12 @@
 
 val class_val =
   Parse_Spec.class_expression --
-    Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
+    Scan.optional (@{keyword +} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   Scan.repeat1 Parse_Spec.context_element >> pair [];
 
 val _ =
   Outer_Syntax.command @{command_keyword class} "define type class"
-   (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
+   (Parse.binding -- Scan.optional (@{keyword =} |-- class_val) ([], []) -- Parse.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
         Toplevel.begin_local_theory begin
           (Class_Declaration.class_cmd name supclasses elems #> snd)));
@@ -652,7 +652,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword instance} "prove type arity or subclass relation"
   ((Parse.class --
-    ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
+    ((@{keyword \<subseteq>} || @{keyword <}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
     Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
     Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I)));
 
@@ -666,8 +666,8 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword overloading} "overloaded definitions"
-   (Scan.repeat1 (Parse.name --| (@{keyword "=="} || @{keyword "\<equiv>"}) -- Parse.term --
-      Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
+   (Scan.repeat1 (Parse.name --| (@{keyword ==} || @{keyword \<equiv>}) -- Parse.term --
+      Scan.optional (@{keyword "("} |-- (@{keyword unchecked} >> K false) --| @{keyword ")"}) true
       >> Scan.triple1) --| Parse.begin
    >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
 
@@ -787,7 +787,7 @@
     (Parse.and_list1
       (Parse_Spec.opt_thm_name ":" --
         ((Parse.binding -- Parse.opt_mixfix) --
-          ((@{keyword "\<equiv>"} || @{keyword "=="}) |-- Parse.!!! Parse.termp)))
+          ((@{keyword \<equiv>} || @{keyword ==}) |-- Parse.!!! Parse.termp)))
     >> (fn args => Toplevel.proof (fn state =>
         (legacy_feature "Old 'def' command -- use 'define' instead"; Proof.def_cmd args state))));
 
@@ -806,7 +806,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword let} "bind text variables"
-    (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
+    (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword =} |-- Parse.term))
       >> (Toplevel.proof o Proof.let_bind_cmd));
 
 val _ =
@@ -937,7 +937,7 @@
 
 val for_params =
   Scan.optional
-    (@{keyword "for"} |--
+    (@{keyword for} |--
       Parse.!!! ((Scan.option Parse.dots >> is_some) --
         (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
     (false, []);
@@ -945,7 +945,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword subgoal}
     "focus on first subgoal within backward refinement"
-    (opt_fact_binding -- (Scan.option (@{keyword "premises"} |-- Parse.!!! opt_fact_binding)) --
+    (opt_fact_binding -- (Scan.option (@{keyword premises} |-- Parse.!!! opt_fact_binding)) --
       for_params >> (fn ((a, b), c) =>
         Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
 
@@ -1176,7 +1176,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword typ} "read and print type"
-    (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
+    (opt_modes -- (Parse.typ -- Scan.option (@{keyword ::} |-- Parse.!!! Parse.sort))
       >> Isar_Cmd.print_type);
 
 val _ =