prefer control symbol antiquotations;
authorwenzelm
Wed Dec 06 18:59:33 2017 +0100 (4 months ago)
changeset 67147dea94b1aabc3
parent 67146 909dcdec2122
child 67148 d24dcac5eb4c
prefer control symbol antiquotations;
src/Pure/Isar/attrib.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/class.ML
src/Pure/Isar/code.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/overloading.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/ML/ml_thms.ML
src/Pure/ML_Bootstrap.thy
src/Pure/PIDE/resources.ML
src/Pure/Proof/extraction.ML
src/Pure/Pure.thy
src/Pure/Thy/document_antiquotations.ML
src/Pure/Thy/term_style.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/bibtex.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/jedit.ML
src/Pure/Tools/named_theorems.ML
src/Pure/Tools/plugin.ML
src/Pure/Tools/rail.ML
src/Pure/Tools/rule_insts.ML
src/Pure/Tools/simplifier_trace.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Wed Dec 06 15:46:35 2017 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Dec 06 18:59:33 2017 +0100
     1.3 @@ -489,38 +489,38 @@
     1.4  (* theory setup *)
     1.5  
     1.6  val _ = Theory.setup
     1.7 - (setup @{binding tagged} (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
     1.8 -  setup @{binding untagged} (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
     1.9 -  setup @{binding kind} (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
    1.10 -  setup @{binding THEN}
    1.11 + (setup \<^binding>\<open>tagged\<close> (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
    1.12 +  setup \<^binding>\<open>untagged\<close> (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
    1.13 +  setup \<^binding>\<open>kind\<close> (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
    1.14 +  setup \<^binding>\<open>THEN\<close>
    1.15      (Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
    1.16        >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B))))
    1.17      "resolution with rule" #>
    1.18 -  setup @{binding OF}
    1.19 +  setup \<^binding>\<open>OF\<close>
    1.20      (thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs)))
    1.21      "rule resolved with facts" #>
    1.22 -  setup @{binding rename_abs}
    1.23 +  setup \<^binding>\<open>rename_abs\<close>
    1.24      (Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
    1.25        Thm.rule_attribute [] (K (Drule.rename_bvars' vs))))
    1.26      "rename bound variables in abstractions" #>
    1.27 -  setup @{binding unfolded}
    1.28 +  setup \<^binding>\<open>unfolded\<close>
    1.29      (thms >> (fn ths =>
    1.30        Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths)))
    1.31      "unfolded definitions" #>
    1.32 -  setup @{binding folded}
    1.33 +  setup \<^binding>\<open>folded\<close>
    1.34      (thms >> (fn ths =>
    1.35        Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths)))
    1.36      "folded definitions" #>
    1.37 -  setup @{binding consumes}
    1.38 +  setup \<^binding>\<open>consumes\<close>
    1.39      (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
    1.40      "number of consumed facts" #>
    1.41 -  setup @{binding constraints}
    1.42 +  setup \<^binding>\<open>constraints\<close>
    1.43      (Scan.lift Parse.nat >> Rule_Cases.constraints)
    1.44      "number of equality constraints" #>
    1.45 -  setup @{binding cases_open}
    1.46 +  setup \<^binding>\<open>cases_open\<close>
    1.47      (Scan.succeed Rule_Cases.cases_open)
    1.48      "rule with open parameters" #>
    1.49 -  setup @{binding case_names}
    1.50 +  setup \<^binding>\<open>case_names\<close>
    1.51      (Scan.lift (Scan.repeat (Args.name --
    1.52        Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") []))
    1.53        >> (fn cs =>
    1.54 @@ -528,37 +528,37 @@
    1.55            (map #1 cs)
    1.56            (map (map (the_default Rule_Cases.case_hypsN) o #2) cs)))
    1.57      "named rule cases" #>
    1.58 -  setup @{binding case_conclusion}
    1.59 +  setup \<^binding>\<open>case_conclusion\<close>
    1.60      (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
    1.61      "named conclusion of rule cases" #>
    1.62 -  setup @{binding params}
    1.63 +  setup \<^binding>\<open>params\<close>
    1.64      (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
    1.65      "named rule parameters" #>
    1.66 -  setup @{binding rule_format}
    1.67 +  setup \<^binding>\<open>rule_format\<close>
    1.68      (Scan.lift (Args.mode "no_asm")
    1.69        >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format))
    1.70      "result put into canonical rule format" #>
    1.71 -  setup @{binding elim_format}
    1.72 +  setup \<^binding>\<open>elim_format\<close>
    1.73      (Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim)))
    1.74      "destruct rule turned into elimination rule format" #>
    1.75 -  setup @{binding no_vars}
    1.76 +  setup \<^binding>\<open>no_vars\<close>
    1.77      (Scan.succeed (Thm.rule_attribute [] (fn context => fn th =>
    1.78        let
    1.79          val ctxt = Variable.set_body false (Context.proof_of context);
    1.80          val ((_, [th']), _) = Variable.import true [th] ctxt;
    1.81        in th' end)))
    1.82      "imported schematic variables" #>
    1.83 -  setup @{binding atomize}
    1.84 +  setup \<^binding>\<open>atomize\<close>
    1.85      (Scan.succeed Object_Logic.declare_atomize) "declaration of atomize rule" #>
    1.86 -  setup @{binding rulify}
    1.87 +  setup \<^binding>\<open>rulify\<close>
    1.88      (Scan.succeed Object_Logic.declare_rulify) "declaration of rulify rule" #>
    1.89 -  setup @{binding rotated}
    1.90 +  setup \<^binding>\<open>rotated\<close>
    1.91      (Scan.lift (Scan.optional Parse.int 1
    1.92        >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))) "rotated theorem premises" #>
    1.93 -  setup @{binding defn}
    1.94 +  setup \<^binding>\<open>defn\<close>
    1.95      (add_del Local_Defs.defn_add Local_Defs.defn_del)
    1.96      "declaration of definitional transformations" #>
    1.97 -  setup @{binding abs_def}
    1.98 +  setup \<^binding>\<open>abs_def\<close>
    1.99      (Scan.succeed (Thm.rule_attribute [] (Local_Defs.abs_def_rule o Context.proof_of)))
   1.100      "abstract over free variables of definitional theorem" #>
   1.101  
     2.1 --- a/src/Pure/Isar/calculation.ML	Wed Dec 06 15:46:35 2017 +0100
     2.2 +++ b/src/Pure/Isar/calculation.ML	Wed Dec 06 18:59:33 2017 +0100
     2.3 @@ -126,11 +126,11 @@
     2.4  (* concrete syntax *)
     2.5  
     2.6  val _ = Theory.setup
     2.7 - (Attrib.setup @{binding trans} (Attrib.add_del trans_add trans_del)
     2.8 + (Attrib.setup \<^binding>\<open>trans\<close> (Attrib.add_del trans_add trans_del)
     2.9      "declaration of transitivity rule" #>
    2.10 -  Attrib.setup @{binding sym} (Attrib.add_del sym_add sym_del)
    2.11 +  Attrib.setup \<^binding>\<open>sym\<close> (Attrib.add_del sym_add sym_del)
    2.12      "declaration of symmetry rule" #>
    2.13 -  Attrib.setup @{binding symmetric} (Scan.succeed symmetric)
    2.14 +  Attrib.setup \<^binding>\<open>symmetric\<close> (Scan.succeed symmetric)
    2.15      "resolution with symmetry rule" #>
    2.16    Global_Theory.add_thms
    2.17     [((Binding.empty, transitive_thm), [trans_add]),
     3.1 --- a/src/Pure/Isar/class.ML	Wed Dec 06 15:46:35 2017 +0100
     3.2 +++ b/src/Pure/Isar/class.ML	Wed Dec 06 18:59:33 2017 +0100
     3.3 @@ -782,9 +782,9 @@
     3.4    standard_intro_classes_tac ctxt facts;
     3.5  
     3.6  val _ = Theory.setup
     3.7 - (Method.setup @{binding intro_classes} (Scan.succeed (METHOD o intro_classes_tac))
     3.8 + (Method.setup \<^binding>\<open>intro_classes\<close> (Scan.succeed (METHOD o intro_classes_tac))
     3.9      "back-chain introduction rules of classes" #>
    3.10 -  Method.setup @{binding standard} (Scan.succeed (METHOD o standard_tac))
    3.11 +  Method.setup \<^binding>\<open>standard\<close> (Scan.succeed (METHOD o standard_tac))
    3.12      "standard proof step: Pure intro/elim rule or class introduction");
    3.13  
    3.14  
     4.1 --- a/src/Pure/Isar/code.ML	Wed Dec 06 15:46:35 2017 +0100
     4.2 +++ b/src/Pure/Isar/code.ML	Wed Dec 06 18:59:33 2017 +0100
     4.3 @@ -1264,7 +1264,7 @@
     4.4  
     4.5  structure Codetype_Plugin = Plugin(type T = string);
     4.6  
     4.7 -val codetype_plugin = Plugin_Name.declare_setup @{binding codetype};
     4.8 +val codetype_plugin = Plugin_Name.declare_setup \<^binding>\<open>codetype\<close>;
     4.9  
    4.10  fun type_interpretation f =
    4.11    Codetype_Plugin.interpretation codetype_plugin
    4.12 @@ -1539,7 +1539,7 @@
    4.13        || Scan.succeed (code_attribute
    4.14            add_maybe_abs_eqn_liberal);
    4.15    in
    4.16 -    Attrib.setup @{binding code} (Scan.lift code_attribute_parser)
    4.17 +    Attrib.setup \<^binding>\<open>code\<close> (Scan.lift code_attribute_parser)
    4.18          "declare theorems for code generation"
    4.19    end);
    4.20  
     5.1 --- a/src/Pure/Isar/context_rules.ML	Wed Dec 06 15:46:35 2017 +0100
     5.2 +++ b/src/Pure/Isar/context_rules.ML	Wed Dec 06 18:59:33 2017 +0100
     5.3 @@ -219,13 +219,13 @@
     5.4      Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
     5.5  
     5.6  val _ = Theory.setup
     5.7 - (Attrib.setup @{binding intro} (add intro_bang intro intro_query)
     5.8 + (Attrib.setup \<^binding>\<open>intro\<close> (add intro_bang intro intro_query)
     5.9      "declaration of introduction rule" #>
    5.10 -  Attrib.setup @{binding elim} (add elim_bang elim elim_query)
    5.11 +  Attrib.setup \<^binding>\<open>elim\<close> (add elim_bang elim elim_query)
    5.12      "declaration of elimination rule" #>
    5.13 -  Attrib.setup @{binding dest} (add dest_bang dest dest_query)
    5.14 +  Attrib.setup \<^binding>\<open>dest\<close> (add dest_bang dest dest_query)
    5.15      "declaration of destruction rule" #>
    5.16 -  Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
    5.17 +  Attrib.setup \<^binding>\<open>rule\<close> (Scan.lift Args.del >> K rule_del)
    5.18      "remove declaration of intro/elim/dest rule");
    5.19  
    5.20  end;
     6.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 06 15:46:35 2017 +0100
     6.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Dec 06 18:59:33 2017 +0100
     6.3 @@ -211,9 +211,9 @@
     6.4  val diag_goal = Proof.goal o Toplevel.proof_of o diag_state;
     6.5  
     6.6  val _ = Theory.setup
     6.7 -  (ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state})
     6.8 +  (ML_Antiquotation.value (Binding.qualify true "Isar" \<^binding>\<open>state\<close>)
     6.9      (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
    6.10 -   ML_Antiquotation.value (Binding.qualify true "Isar" @{binding goal})
    6.11 +   ML_Antiquotation.value (Binding.qualify true "Isar" \<^binding>\<open>goal\<close>)
    6.12      (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
    6.13  
    6.14  
     7.1 --- a/src/Pure/Isar/locale.ML	Wed Dec 06 15:46:35 2017 +0100
     7.2 +++ b/src/Pure/Isar/locale.ML	Wed Dec 06 18:59:33 2017 +0100
     7.3 @@ -678,9 +678,9 @@
     7.4  val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
     7.5  
     7.6  val _ = Theory.setup
     7.7 - (Method.setup @{binding intro_locales} (Scan.succeed (METHOD o try_intro_locales_tac false))
     7.8 + (Method.setup \<^binding>\<open>intro_locales\<close> (Scan.succeed (METHOD o try_intro_locales_tac false))
     7.9      "back-chain introduction rules of locales without unfolding predicates" #>
    7.10 -  Method.setup @{binding unfold_locales} (Scan.succeed (METHOD o try_intro_locales_tac true))
    7.11 +  Method.setup \<^binding>\<open>unfold_locales\<close> (Scan.succeed (METHOD o try_intro_locales_tac true))
    7.12      "back-chain all introduction rules of locales");
    7.13  
    7.14  
     8.1 --- a/src/Pure/Isar/method.ML	Wed Dec 06 15:46:35 2017 +0100
     8.2 +++ b/src/Pure/Isar/method.ML	Wed Dec 06 18:59:33 2017 +0100
     8.3 @@ -266,7 +266,7 @@
     8.4  
     8.5  (* rule etc. -- single-step refinements *)
     8.6  
     8.7 -val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false);
     8.8 +val rule_trace = Attrib.setup_config_bool \<^binding>\<open>rule_trace\<close> (fn _ => false);
     8.9  
    8.10  fun trace ctxt rules =
    8.11    if Config.get ctxt rule_trace andalso not (null rules) then
    8.12 @@ -795,13 +795,13 @@
    8.13  (* theory setup *)
    8.14  
    8.15  val _ = Theory.setup
    8.16 - (setup @{binding fail} (Scan.succeed (K fail)) "force failure" #>
    8.17 -  setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #>
    8.18 -  setup @{binding sleep} (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s)))
    8.19 + (setup \<^binding>\<open>fail\<close> (Scan.succeed (K fail)) "force failure" #>
    8.20 +  setup \<^binding>\<open>succeed\<close> (Scan.succeed (K succeed)) "succeed" #>
    8.21 +  setup \<^binding>\<open>sleep\<close> (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s)))
    8.22      "succeed after delay (in seconds)" #>
    8.23 -  setup @{binding "-"} (Scan.succeed (K (SIMPLE_METHOD all_tac)))
    8.24 +  setup \<^binding>\<open>-\<close> (Scan.succeed (K (SIMPLE_METHOD all_tac)))
    8.25      "insert current facts, nothing else" #>
    8.26 -  setup @{binding goal_cases} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn _ =>
    8.27 +  setup \<^binding>\<open>goal_cases\<close> (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn _ =>
    8.28      CONTEXT_METHOD (fn _ => fn (ctxt, st) =>
    8.29        (case drop (Thm.nprems_of st) names of
    8.30          [] => NONE
    8.31 @@ -813,36 +813,36 @@
    8.32        |> (fn SOME msg => Seq.single (Seq.Error msg)
    8.33             | NONE => goal_cases_tac (map Token.content_of names) (ctxt, st)))))
    8.34      "bind cases for goals" #>
    8.35 -  setup @{binding insert} (Attrib.thms >> (K o insert))
    8.36 +  setup \<^binding>\<open>insert\<close> (Attrib.thms >> (K o insert))
    8.37      "insert theorems, ignoring facts" #>
    8.38 -  setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
    8.39 +  setup \<^binding>\<open>intro\<close> (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
    8.40      "repeatedly apply introduction rules" #>
    8.41 -  setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths))
    8.42 +  setup \<^binding>\<open>elim\<close> (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths))
    8.43      "repeatedly apply elimination rules" #>
    8.44 -  setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #>
    8.45 -  setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #>
    8.46 -  setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize)
    8.47 +  setup \<^binding>\<open>unfold\<close> (Attrib.thms >> unfold_meth) "unfold definitions" #>
    8.48 +  setup \<^binding>\<open>fold\<close> (Attrib.thms >> fold_meth) "fold definitions" #>
    8.49 +  setup \<^binding>\<open>atomize\<close> (Scan.lift (Args.mode "full") >> atomize)
    8.50      "present local premises as object-level statements" #>
    8.51 -  setup @{binding rule} (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
    8.52 +  setup \<^binding>\<open>rule\<close> (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
    8.53      "apply some intro/elim rule" #>
    8.54 -  setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #>
    8.55 -  setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #>
    8.56 -  setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #>
    8.57 -  setup @{binding this} (Scan.succeed this) "apply current facts as rules" #>
    8.58 -  setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #>
    8.59 -  setup @{binding assumption} (Scan.succeed assumption)
    8.60 +  setup \<^binding>\<open>erule\<close> (xrule_meth erule) "apply rule in elimination manner (improper)" #>
    8.61 +  setup \<^binding>\<open>drule\<close> (xrule_meth drule) "apply rule in destruct manner (improper)" #>
    8.62 +  setup \<^binding>\<open>frule\<close> (xrule_meth frule) "apply rule in forward manner (improper)" #>
    8.63 +  setup \<^binding>\<open>this\<close> (Scan.succeed this) "apply current facts as rules" #>
    8.64 +  setup \<^binding>\<open>fact\<close> (Attrib.thms >> fact) "composition by facts from context" #>
    8.65 +  setup \<^binding>\<open>assumption\<close> (Scan.succeed assumption)
    8.66      "proof by assumption, preferring facts" #>
    8.67 -  setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
    8.68 +  setup \<^binding>\<open>rename_tac\<close> (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
    8.69      (fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs))))
    8.70      "rename parameters of goal" #>
    8.71 -  setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
    8.72 +  setup \<^binding>\<open>rotate_tac\<close> (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
    8.73      (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
    8.74        "rotate assumptions of goal" #>
    8.75 -  setup @{binding tactic} (parse_tactic >> (K o METHOD))
    8.76 +  setup \<^binding>\<open>tactic\<close> (parse_tactic >> (K o METHOD))
    8.77      "ML tactic as proof method" #>
    8.78 -  setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac))
    8.79 +  setup \<^binding>\<open>raw_tactic\<close> (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac))
    8.80      "ML tactic as raw proof method" #>
    8.81 -  setup @{binding use}
    8.82 +  setup \<^binding>\<open>use\<close>
    8.83      (Attrib.thms -- (Scan.lift (Parse.$$$ "in") |-- text_closure) >>
    8.84        (fn (thms, text) => fn ctxt => fn _ => evaluate_runtime text ctxt thms))
    8.85      "indicate method facts and context for method expression");
     9.1 --- a/src/Pure/Isar/overloading.ML	Wed Dec 06 15:46:35 2017 +0100
     9.2 +++ b/src/Pure/Isar/overloading.ML	Wed Dec 06 18:59:33 2017 +0100
     9.3 @@ -92,7 +92,7 @@
     9.4    | SOME t' => if t aconv t' then NONE else SOME t');
     9.5  
     9.6  val show_reverted_improvements =
     9.7 -  Attrib.setup_config_bool @{binding "show_reverted_improvements"} (K true);
     9.8 +  Attrib.setup_config_bool \<^binding>\<open>show_reverted_improvements\<close> (K true);
     9.9  
    9.10  fun improve_term_uncheck ts ctxt =
    9.11    let
    10.1 --- a/src/Pure/ML/ml_antiquotations.ML	Wed Dec 06 15:46:35 2017 +0100
    10.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Wed Dec 06 18:59:33 2017 +0100
    10.3 @@ -10,13 +10,13 @@
    10.4  (* ML support *)
    10.5  
    10.6  val _ = Theory.setup
    10.7 - (ML_Antiquotation.inline @{binding undefined}
    10.8 + (ML_Antiquotation.inline \<^binding>\<open>undefined\<close>
    10.9      (Scan.succeed "(raise General.Match)") #>
   10.10  
   10.11 -  ML_Antiquotation.inline @{binding assert}
   10.12 +  ML_Antiquotation.inline \<^binding>\<open>assert\<close>
   10.13      (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
   10.14  
   10.15 -  ML_Antiquotation.declaration @{binding print}
   10.16 +  ML_Antiquotation.declaration \<^binding>\<open>print\<close>
   10.17      (Scan.lift (Scan.optional Args.embedded "Output.writeln"))
   10.18        (fn src => fn output => fn ctxt =>
   10.19          let
   10.20 @@ -31,7 +31,7 @@
   10.21              "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))";
   10.22          in (K (env, body), ctxt') end) #>
   10.23  
   10.24 -  ML_Antiquotation.value @{binding rat}
   10.25 +  ML_Antiquotation.value \<^binding>\<open>rat\<close>
   10.26      (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat --
   10.27        Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) =>
   10.28          "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))))
   10.29 @@ -40,7 +40,7 @@
   10.30  (* formal entities *)
   10.31  
   10.32  val _ = Theory.setup
   10.33 - (ML_Antiquotation.value @{binding system_option}
   10.34 + (ML_Antiquotation.value \<^binding>\<open>system_option\<close>
   10.35      (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
   10.36        let
   10.37          val markup =
   10.38 @@ -56,35 +56,35 @@
   10.39          val _ = Context_Position.report ctxt pos markup;
   10.40        in ML_Syntax.print_string name end)) #>
   10.41  
   10.42 -  ML_Antiquotation.value @{binding theory}
   10.43 +  ML_Antiquotation.value \<^binding>\<open>theory\<close>
   10.44      (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
   10.45        (Theory.check ctxt (name, pos);
   10.46         "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
   10.47      || Scan.succeed "Proof_Context.theory_of ML_context") #>
   10.48  
   10.49 -  ML_Antiquotation.value @{binding theory_context}
   10.50 +  ML_Antiquotation.value \<^binding>\<open>theory_context\<close>
   10.51      (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
   10.52        (Theory.check ctxt (name, pos);
   10.53         "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
   10.54          ML_Syntax.print_string name))) #>
   10.55  
   10.56 -  ML_Antiquotation.inline @{binding context}
   10.57 +  ML_Antiquotation.inline \<^binding>\<open>context\<close>
   10.58      (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #>
   10.59  
   10.60 -  ML_Antiquotation.inline @{binding typ} (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
   10.61 -  ML_Antiquotation.inline @{binding term} (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
   10.62 -  ML_Antiquotation.inline @{binding prop} (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
   10.63 +  ML_Antiquotation.inline \<^binding>\<open>typ\<close> (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
   10.64 +  ML_Antiquotation.inline \<^binding>\<open>term\<close> (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
   10.65 +  ML_Antiquotation.inline \<^binding>\<open>prop\<close> (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
   10.66  
   10.67 -  ML_Antiquotation.value @{binding ctyp} (Args.typ >> (fn T =>
   10.68 +  ML_Antiquotation.value \<^binding>\<open>ctyp\<close> (Args.typ >> (fn T =>
   10.69      "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
   10.70  
   10.71 -  ML_Antiquotation.value @{binding cterm} (Args.term >> (fn t =>
   10.72 +  ML_Antiquotation.value \<^binding>\<open>cterm\<close> (Args.term >> (fn t =>
   10.73      "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
   10.74  
   10.75 -  ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t =>
   10.76 +  ML_Antiquotation.value \<^binding>\<open>cprop\<close> (Args.prop >> (fn t =>
   10.77      "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
   10.78  
   10.79 -  ML_Antiquotation.inline @{binding method}
   10.80 +  ML_Antiquotation.inline \<^binding>\<open>method\<close>
   10.81      (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
   10.82        ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
   10.83  
   10.84 @@ -92,7 +92,7 @@
   10.85  (* locales *)
   10.86  
   10.87  val _ = Theory.setup
   10.88 - (ML_Antiquotation.inline @{binding locale}
   10.89 + (ML_Antiquotation.inline \<^binding>\<open>locale\<close>
   10.90     (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
   10.91        Locale.check (Proof_Context.theory_of ctxt) (name, pos)
   10.92        |> ML_Syntax.print_string)));
   10.93 @@ -106,10 +106,10 @@
   10.94    |> ML_Syntax.print_string);
   10.95  
   10.96  val _ = Theory.setup
   10.97 - (ML_Antiquotation.inline @{binding class} (class false) #>
   10.98 -  ML_Antiquotation.inline @{binding class_syntax} (class true) #>
   10.99 + (ML_Antiquotation.inline \<^binding>\<open>class\<close> (class false) #>
  10.100 +  ML_Antiquotation.inline \<^binding>\<open>class_syntax\<close> (class true) #>
  10.101  
  10.102 -  ML_Antiquotation.inline @{binding sort}
  10.103 +  ML_Antiquotation.inline \<^binding>\<open>sort\<close>
  10.104      (Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
  10.105        ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
  10.106  
  10.107 @@ -128,13 +128,13 @@
  10.108      in ML_Syntax.print_string res end);
  10.109  
  10.110  val _ = Theory.setup
  10.111 - (ML_Antiquotation.inline @{binding type_name}
  10.112 + (ML_Antiquotation.inline \<^binding>\<open>type_name\<close>
  10.113      (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
  10.114 -  ML_Antiquotation.inline @{binding type_abbrev}
  10.115 +  ML_Antiquotation.inline \<^binding>\<open>type_abbrev\<close>
  10.116      (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
  10.117 -  ML_Antiquotation.inline @{binding nonterminal}
  10.118 +  ML_Antiquotation.inline \<^binding>\<open>nonterminal\<close>
  10.119      (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
  10.120 -  ML_Antiquotation.inline @{binding type_syntax}
  10.121 +  ML_Antiquotation.inline \<^binding>\<open>type_syntax\<close>
  10.122      (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
  10.123  
  10.124  
  10.125 @@ -149,20 +149,20 @@
  10.126      in ML_Syntax.print_string res end);
  10.127  
  10.128  val _ = Theory.setup
  10.129 - (ML_Antiquotation.inline @{binding const_name}
  10.130 + (ML_Antiquotation.inline \<^binding>\<open>const_name\<close>
  10.131      (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
  10.132 -  ML_Antiquotation.inline @{binding const_abbrev}
  10.133 +  ML_Antiquotation.inline \<^binding>\<open>const_abbrev\<close>
  10.134      (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
  10.135 -  ML_Antiquotation.inline @{binding const_syntax}
  10.136 +  ML_Antiquotation.inline \<^binding>\<open>const_syntax\<close>
  10.137      (const_name (fn (_, c) => Lexicon.mark_const c)) #>
  10.138  
  10.139 -  ML_Antiquotation.inline @{binding syntax_const}
  10.140 +  ML_Antiquotation.inline \<^binding>\<open>syntax_const\<close>
  10.141      (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (c, pos)) =>
  10.142        if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
  10.143        then ML_Syntax.print_string c
  10.144        else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
  10.145  
  10.146 -  ML_Antiquotation.inline @{binding const}
  10.147 +  ML_Antiquotation.inline \<^binding>\<open>const\<close>
  10.148      (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional
  10.149          (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
  10.150        >> (fn ((ctxt, (raw_c, pos)), Ts) =>
  10.151 @@ -201,7 +201,7 @@
  10.152  in
  10.153  
  10.154  val _ = Theory.setup
  10.155 - (ML_Antiquotation.value @{binding map}
  10.156 + (ML_Antiquotation.value \<^binding>\<open>map\<close>
  10.157      (Scan.lift parameter >> (fn n =>
  10.158        "fn f =>\n\
  10.159        \  let\n\
  10.160 @@ -209,7 +209,7 @@
  10.161        \      | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\
  10.162        \      | map _" ^  dummy n ^ " = raise ListPair.UnequalLengths\n" ^
  10.163        "  in map f end")) #>
  10.164 -  ML_Antiquotation.value @{binding fold}
  10.165 +  ML_Antiquotation.value \<^binding>\<open>fold\<close>
  10.166      (Scan.lift parameter >> (fn n =>
  10.167        "fn f =>\n\
  10.168        \  let\n\
  10.169 @@ -217,7 +217,7 @@
  10.170        \      | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\
  10.171        \      | fold _" ^  dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^
  10.172        "  in fold f end")) #>
  10.173 -  ML_Antiquotation.value @{binding fold_map}
  10.174 +  ML_Antiquotation.value \<^binding>\<open>fold_map\<close>
  10.175      (Scan.lift parameter >> (fn n =>
  10.176        "fn f =>\n\
  10.177        \  let\n\
  10.178 @@ -229,7 +229,7 @@
  10.179        \          in (x :: xs, a'') end\n\
  10.180        \      | fold_map _" ^  dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^
  10.181        "  in fold_map f end")) #>
  10.182 -  ML_Antiquotation.value @{binding split_list}
  10.183 +  ML_Antiquotation.value \<^binding>\<open>split_list\<close>
  10.184      (Scan.lift parameter >> (fn n =>
  10.185        "fn list =>\n\
  10.186        \  let\n\
  10.187 @@ -238,7 +238,7 @@
  10.188        \          let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\
  10.189        \          in " ^ cons_tuple n ^ "end\n\
  10.190        \  in split_list list end")) #>
  10.191 -  ML_Antiquotation.value @{binding apply}
  10.192 +  ML_Antiquotation.value \<^binding>\<open>apply\<close>
  10.193      (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >>
  10.194        (fn (n, opt_index) =>
  10.195          let
  10.196 @@ -259,14 +259,14 @@
  10.197  (* outer syntax *)
  10.198  
  10.199  val _ = Theory.setup
  10.200 - (ML_Antiquotation.value @{binding keyword}
  10.201 + (ML_Antiquotation.value \<^binding>\<open>keyword\<close>
  10.202      (Args.context -- Scan.lift (Parse.position (Parse.embedded || Parse.keyword_with (K true)))
  10.203        >> (fn (ctxt, (name, pos)) =>
  10.204          if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then
  10.205            (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name);
  10.206             "Parse.$$$ " ^ ML_Syntax.print_string name)
  10.207          else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
  10.208 -  ML_Antiquotation.value @{binding command_keyword}
  10.209 +  ML_Antiquotation.value \<^binding>\<open>command_keyword\<close>
  10.210      (Args.context -- Scan.lift (Parse.position Parse.embedded) >> (fn (ctxt, (name, pos)) =>
  10.211        (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
  10.212          SOME markup =>
    11.1 --- a/src/Pure/ML/ml_thms.ML	Wed Dec 06 15:46:35 2017 +0100
    11.2 +++ b/src/Pure/ML/ml_thms.ML	Wed Dec 06 18:59:33 2017 +0100
    11.3 @@ -40,7 +40,7 @@
    11.4  (* attribute source *)
    11.5  
    11.6  val _ = Theory.setup
    11.7 -  (ML_Antiquotation.declaration @{binding attributes} Attrib.attribs
    11.8 +  (ML_Antiquotation.declaration \<^binding>\<open>attributes\<close> Attrib.attribs
    11.9      (fn _ => fn srcs => fn ctxt =>
   11.10        let val i = serial () in
   11.11          ctxt
   11.12 @@ -69,8 +69,8 @@
   11.13    in (decl, ctxt'') end;
   11.14  
   11.15  val _ = Theory.setup
   11.16 -  (ML_Antiquotation.declaration @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
   11.17 -   ML_Antiquotation.declaration @{binding thms} Attrib.thms (K (thm_binding "thms" false)));
   11.18 +  (ML_Antiquotation.declaration \<^binding>\<open>thm\<close> (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
   11.19 +   ML_Antiquotation.declaration \<^binding>\<open>thms\<close> Attrib.thms (K (thm_binding "thms" false)));
   11.20  
   11.21  
   11.22  (* ad-hoc goals *)
   11.23 @@ -80,7 +80,7 @@
   11.24  val goal = Scan.unless (by || and_) Args.embedded_inner_syntax;
   11.25  
   11.26  val _ = Theory.setup
   11.27 -  (ML_Antiquotation.declaration @{binding lemma}
   11.28 +  (ML_Antiquotation.declaration \<^binding>\<open>lemma\<close>
   11.29      (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
   11.30        (Parse.position by -- Method.parse -- Scan.option Method.parse)))
   11.31      (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt =>
    12.1 --- a/src/Pure/ML_Bootstrap.thy	Wed Dec 06 15:46:35 2017 +0100
    12.2 +++ b/src/Pure/ML_Bootstrap.thy	Wed Dec 06 18:59:33 2017 +0100
    12.3 @@ -34,7 +34,7 @@
    12.4      \<close>
    12.5  \<close>
    12.6  
    12.7 -ML \<open>@{assert} (not (can ML \<open>open RunCall\<close>))\<close>
    12.8 +ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close>
    12.9  
   12.10  
   12.11  subsection \<open>Switch to bootstrap environment\<close>
    13.1 --- a/src/Pure/PIDE/resources.ML	Wed Dec 06 15:46:35 2017 +0100
    13.2 +++ b/src/Pure/PIDE/resources.ML	Wed Dec 06 18:59:33 2017 +0100
    13.3 @@ -229,19 +229,19 @@
    13.4  in
    13.5  
    13.6  val _ = Theory.setup
    13.7 - (Thy_Output.antiquotation @{binding path} (Scan.lift (Parse.position Parse.path))
    13.8 + (Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
    13.9      (document_antiq NONE o #context) #>
   13.10 -  Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
   13.11 +  Thy_Output.antiquotation \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
   13.12      (document_antiq (SOME File.check_file) o #context) #>
   13.13 -  Thy_Output.antiquotation @{binding dir} (Scan.lift (Parse.position Parse.path))
   13.14 +  Thy_Output.antiquotation \<^binding>\<open>dir\<close> (Scan.lift (Parse.position Parse.path))
   13.15      (document_antiq (SOME File.check_dir) o #context) #>
   13.16 -  ML_Antiquotation.value @{binding path}
   13.17 +  ML_Antiquotation.value \<^binding>\<open>path\<close>
   13.18      (Args.context -- Scan.lift (Parse.position Parse.path)
   13.19        >> uncurry (ML_antiq NONE)) #>
   13.20 -  ML_Antiquotation.value @{binding file}
   13.21 +  ML_Antiquotation.value \<^binding>\<open>file\<close>
   13.22      (Args.context -- Scan.lift (Parse.position Parse.path)
   13.23        >> uncurry (ML_antiq (SOME File.check_file))) #>
   13.24 -  ML_Antiquotation.value @{binding dir}
   13.25 +  ML_Antiquotation.value \<^binding>\<open>dir\<close>
   13.26      (Args.context -- Scan.lift (Parse.position Parse.path)
   13.27        >> uncurry (ML_antiq (SOME File.check_dir))));
   13.28  
    14.1 --- a/src/Pure/Proof/extraction.ML	Wed Dec 06 15:46:35 2017 +0100
    14.2 +++ b/src/Pure/Proof/extraction.ML	Wed Dec 06 18:59:33 2017 +0100
    14.3 @@ -470,9 +470,9 @@
    14.4        "(realizes (r) (!!x. PROP P (x))) ==  \
    14.5      \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
    14.6  
    14.7 -   Attrib.setup @{binding extraction_expand} (Scan.succeed (extraction_expand false))
    14.8 +   Attrib.setup \<^binding>\<open>extraction_expand\<close> (Scan.succeed (extraction_expand false))
    14.9       "specify theorems to be expanded during extraction" #>
   14.10 -   Attrib.setup @{binding extraction_expand_def} (Scan.succeed (extraction_expand true))
   14.11 +   Attrib.setup \<^binding>\<open>extraction_expand_def\<close> (Scan.succeed (extraction_expand true))
   14.12       "specify definitions to be expanded during extraction");
   14.13  
   14.14  
    15.1 --- a/src/Pure/Pure.thy	Wed Dec 06 15:46:35 2017 +0100
    15.2 +++ b/src/Pure/Pure.thy	Wed Dec 06 18:59:33 2017 +0100
    15.3 @@ -110,7 +110,7 @@
    15.4  subsection \<open>External file dependencies\<close>
    15.5  
    15.6  ML \<open>
    15.7 -  Outer_Syntax.command @{command_keyword external_file} "formal dependency on external file"
    15.8 +  Outer_Syntax.command \<^command_keyword>\<open>external_file\<close> "formal dependency on external file"
    15.9      (Parse.position Parse.path >> (fn (s, pos) => Toplevel.keep (fn st =>
   15.10        let
   15.11          val ctxt = Toplevel.context_of st;
   15.12 @@ -126,38 +126,38 @@
   15.13  ML \<open>
   15.14  local
   15.15  
   15.16 -val semi = Scan.option @{keyword ";"};
   15.17 +val semi = Scan.option \<^keyword>\<open>;\<close>;
   15.18  
   15.19  val _ =
   15.20 -  Outer_Syntax.command @{command_keyword ML_file} "read and evaluate Isabelle/ML file"
   15.21 +  Outer_Syntax.command \<^command_keyword>\<open>ML_file\<close> "read and evaluate Isabelle/ML file"
   15.22      (Resources.parse_files "ML_file" --| semi >> ML_File.ML NONE);
   15.23  
   15.24  val _ =
   15.25 -  Outer_Syntax.command @{command_keyword ML_file_debug}
   15.26 +  Outer_Syntax.command \<^command_keyword>\<open>ML_file_debug\<close>
   15.27      "read and evaluate Isabelle/ML file (with debugger information)"
   15.28      (Resources.parse_files "ML_file_debug" --| semi >> ML_File.ML (SOME true));
   15.29  
   15.30  val _ =
   15.31 -  Outer_Syntax.command @{command_keyword ML_file_no_debug}
   15.32 +  Outer_Syntax.command \<^command_keyword>\<open>ML_file_no_debug\<close>
   15.33      "read and evaluate Isabelle/ML file (no debugger information)"
   15.34      (Resources.parse_files "ML_file_no_debug" --| semi >> ML_File.ML (SOME false));
   15.35  
   15.36  val _ =
   15.37 -  Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file"
   15.38 +  Outer_Syntax.command \<^command_keyword>\<open>SML_file\<close> "read and evaluate Standard ML file"
   15.39      (Resources.parse_files "SML_file" --| semi >> ML_File.SML NONE);
   15.40  
   15.41  val _ =
   15.42 -  Outer_Syntax.command @{command_keyword SML_file_debug}
   15.43 +  Outer_Syntax.command \<^command_keyword>\<open>SML_file_debug\<close>
   15.44      "read and evaluate Standard ML file (with debugger information)"
   15.45      (Resources.parse_files "SML_file_debug" --| semi >> ML_File.SML (SOME true));
   15.46  
   15.47  val _ =
   15.48 -  Outer_Syntax.command @{command_keyword SML_file_no_debug}
   15.49 +  Outer_Syntax.command \<^command_keyword>\<open>SML_file_no_debug\<close>
   15.50      "read and evaluate Standard ML file (no debugger information)"
   15.51      (Resources.parse_files "SML_file_no_debug" --| semi >> ML_File.SML (SOME false));
   15.52  
   15.53  val _ =
   15.54 -  Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
   15.55 +  Outer_Syntax.command \<^command_keyword>\<open>SML_export\<close> "evaluate SML within Isabelle/ML environment"
   15.56      (Parse.ML_source >> (fn source =>
   15.57        let
   15.58          val flags: ML_Compiler.flags =
   15.59 @@ -169,7 +169,7 @@
   15.60        end));
   15.61  
   15.62  val _ =
   15.63 -  Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment"
   15.64 +  Outer_Syntax.command \<^command_keyword>\<open>SML_import\<close> "evaluate Isabelle/ML within SML environment"
   15.65      (Parse.ML_source >> (fn source =>
   15.66        let
   15.67          val flags: ML_Compiler.flags =
   15.68 @@ -182,7 +182,7 @@
   15.69        end));
   15.70  
   15.71  val _ =
   15.72 -  Outer_Syntax.command @{command_keyword ML_prf} "ML text within proof"
   15.73 +  Outer_Syntax.command \<^command_keyword>\<open>ML_prf\<close> "ML text within proof"
   15.74      (Parse.ML_source >> (fn source =>
   15.75        Toplevel.proof (Proof.map_context (Context.proof_map
   15.76          (ML_Context.exec (fn () =>
   15.77 @@ -190,52 +190,52 @@
   15.78            Proof.propagate_ml_env)));
   15.79  
   15.80  val _ =
   15.81 -  Outer_Syntax.command @{command_keyword ML_val} "diagnostic ML text"
   15.82 +  Outer_Syntax.command \<^command_keyword>\<open>ML_val\<close> "diagnostic ML text"
   15.83      (Parse.ML_source >> Isar_Cmd.ml_diag true);
   15.84  
   15.85  val _ =
   15.86 -  Outer_Syntax.command @{command_keyword ML_command} "diagnostic ML text (silent)"
   15.87 +  Outer_Syntax.command \<^command_keyword>\<open>ML_command\<close> "diagnostic ML text (silent)"
   15.88      (Parse.ML_source >> Isar_Cmd.ml_diag false);
   15.89  
   15.90  val _ =
   15.91 -  Outer_Syntax.command @{command_keyword setup} "ML setup for global theory"
   15.92 +  Outer_Syntax.command \<^command_keyword>\<open>setup\<close> "ML setup for global theory"
   15.93      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup));
   15.94  
   15.95  val _ =
   15.96 -  Outer_Syntax.local_theory @{command_keyword local_setup} "ML setup for local theory"
   15.97 +  Outer_Syntax.local_theory \<^command_keyword>\<open>local_setup\<close> "ML setup for local theory"
   15.98      (Parse.ML_source >> Isar_Cmd.local_setup);
   15.99  
  15.100  val _ =
  15.101 -  Outer_Syntax.command @{command_keyword oracle} "declare oracle"
  15.102 -    (Parse.range Parse.name -- (@{keyword =} |-- Parse.ML_source) >>
  15.103 +  Outer_Syntax.command \<^command_keyword>\<open>oracle\<close> "declare oracle"
  15.104 +    (Parse.range Parse.name -- (\<^keyword>\<open>=\<close> |-- Parse.ML_source) >>
  15.105        (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
  15.106  
  15.107  val _ =
  15.108 -  Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML"
  15.109 +  Outer_Syntax.local_theory \<^command_keyword>\<open>attribute_setup\<close> "define attribute in ML"
  15.110      (Parse.position Parse.name --
  15.111 -        Parse.!!! (@{keyword =} |-- Parse.ML_source -- Scan.optional Parse.text "")
  15.112 +        Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Scan.optional Parse.text "")
  15.113        >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
  15.114  
  15.115  val _ =
  15.116 -  Outer_Syntax.local_theory @{command_keyword method_setup} "define proof method in ML"
  15.117 +  Outer_Syntax.local_theory \<^command_keyword>\<open>method_setup\<close> "define proof method in ML"
  15.118      (Parse.position Parse.name --
  15.119 -        Parse.!!! (@{keyword =} |-- Parse.ML_source -- Scan.optional Parse.text "")
  15.120 +        Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Scan.optional Parse.text "")
  15.121        >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
  15.122  
  15.123  val _ =
  15.124 -  Outer_Syntax.local_theory @{command_keyword declaration} "generic ML declaration"
  15.125 +  Outer_Syntax.local_theory \<^command_keyword>\<open>declaration\<close> "generic ML declaration"
  15.126      (Parse.opt_keyword "pervasive" -- Parse.ML_source
  15.127        >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
  15.128  
  15.129  val _ =
  15.130 -  Outer_Syntax.local_theory @{command_keyword syntax_declaration} "generic ML syntax declaration"
  15.131 +  Outer_Syntax.local_theory \<^command_keyword>\<open>syntax_declaration\<close> "generic ML syntax declaration"
  15.132      (Parse.opt_keyword "pervasive" -- Parse.ML_source
  15.133        >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
  15.134  
  15.135  val _ =
  15.136 -  Outer_Syntax.local_theory @{command_keyword simproc_setup} "define simproc in ML"
  15.137 +  Outer_Syntax.local_theory \<^command_keyword>\<open>simproc_setup\<close> "define simproc in ML"
  15.138      (Parse.position Parse.name --
  15.139 -      (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword =}) --
  15.140 +      (\<^keyword>\<open>(\<close> |-- Parse.enum1 "|" Parse.term --| \<^keyword>\<open>)\<close> --| \<^keyword>\<open>=\<close>) --
  15.141        Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c));
  15.142  
  15.143  in end\<close>
  15.144 @@ -249,20 +249,20 @@
  15.145  local
  15.146  
  15.147  val _ =
  15.148 -  Outer_Syntax.local_theory @{command_keyword default_sort}
  15.149 +  Outer_Syntax.local_theory \<^command_keyword>\<open>default_sort\<close>
  15.150      "declare default sort for explicit type variables"
  15.151      (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
  15.152  
  15.153  val _ =
  15.154 -  Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
  15.155 +  Outer_Syntax.local_theory \<^command_keyword>\<open>typedecl\<close> "type declaration"
  15.156      (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
  15.157        >> (fn ((args, a), mx) =>
  15.158            Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd));
  15.159  
  15.160  val _ =
  15.161 -  Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
  15.162 +  Outer_Syntax.local_theory \<^command_keyword>\<open>type_synonym\<close> "declare type abbreviation"
  15.163      (Parse.type_args -- Parse.binding --
  15.164 -      (@{keyword =} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
  15.165 +      (\<^keyword>\<open>=\<close> |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
  15.166        >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
  15.167  
  15.168  in end\<close>
  15.169 @@ -274,11 +274,11 @@
  15.170  local
  15.171  
  15.172  val _ =
  15.173 -  Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment"
  15.174 +  Outer_Syntax.command \<^command_keyword>\<open>judgment\<close> "declare object-logic judgment"
  15.175      (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
  15.176  
  15.177  val _ =
  15.178 -  Outer_Syntax.command @{command_keyword consts} "declare constants"
  15.179 +  Outer_Syntax.command \<^command_keyword>\<open>consts\<close> "declare constants"
  15.180      (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
  15.181  
  15.182  in end\<close>
  15.183 @@ -290,40 +290,40 @@
  15.184  local
  15.185  
  15.186  val _ =
  15.187 -  Outer_Syntax.command @{command_keyword nonterminal}
  15.188 +  Outer_Syntax.command \<^command_keyword>\<open>nonterminal\<close>
  15.189      "declare syntactic type constructors (grammar nonterminal symbols)"
  15.190      (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
  15.191  
  15.192  val _ =
  15.193 -  Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses"
  15.194 +  Outer_Syntax.command \<^command_keyword>\<open>syntax\<close> "add raw syntax clauses"
  15.195      (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
  15.196        >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
  15.197  
  15.198  val _ =
  15.199 -  Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses"
  15.200 +  Outer_Syntax.command \<^command_keyword>\<open>no_syntax\<close> "delete raw syntax clauses"
  15.201      (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
  15.202        >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
  15.203  
  15.204  val trans_pat =
  15.205    Scan.optional
  15.206 -    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.name --| @{keyword ")"})) "logic"
  15.207 +    (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.inner_syntax Parse.name --| \<^keyword>\<open>)\<close>)) "logic"
  15.208      -- Parse.inner_syntax Parse.string;
  15.209  
  15.210  fun trans_arrow toks =
  15.211 -  ((@{keyword \<rightharpoonup>} || @{keyword =>}) >> K Syntax.Parse_Rule ||
  15.212 -    (@{keyword \<leftharpoondown>} || @{keyword <=}) >> K Syntax.Print_Rule ||
  15.213 -    (@{keyword \<rightleftharpoons>} || @{keyword ==}) >> K Syntax.Parse_Print_Rule) toks;
  15.214 +  ((\<^keyword>\<open>\<rightharpoonup>\<close> || \<^keyword>\<open>=>\<close>) >> K Syntax.Parse_Rule ||
  15.215 +    (\<^keyword>\<open>\<leftharpoondown>\<close> || \<^keyword>\<open><=\<close>) >> K Syntax.Print_Rule ||
  15.216 +    (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>) >> K Syntax.Parse_Print_Rule) toks;
  15.217  
  15.218  val trans_line =
  15.219    trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
  15.220      >> (fn (left, (arr, right)) => arr (left, right));
  15.221  
  15.222  val _ =
  15.223 -  Outer_Syntax.command @{command_keyword translations} "add syntax translation rules"
  15.224 +  Outer_Syntax.command \<^command_keyword>\<open>translations\<close> "add syntax translation rules"
  15.225      (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
  15.226  
  15.227  val _ =
  15.228 -  Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules"
  15.229 +  Outer_Syntax.command \<^command_keyword>\<open>no_translations\<close> "delete syntax translation rules"
  15.230      (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
  15.231  
  15.232  in end\<close>
  15.233 @@ -335,27 +335,27 @@
  15.234  local
  15.235  
  15.236  val _ =
  15.237 -  Outer_Syntax.command @{command_keyword parse_ast_translation}
  15.238 +  Outer_Syntax.command \<^command_keyword>\<open>parse_ast_translation\<close>
  15.239      "install parse ast translation functions"
  15.240      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
  15.241  
  15.242  val _ =
  15.243 -  Outer_Syntax.command @{command_keyword parse_translation}
  15.244 +  Outer_Syntax.command \<^command_keyword>\<open>parse_translation\<close>
  15.245      "install parse translation functions"
  15.246      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation));
  15.247  
  15.248  val _ =
  15.249 -  Outer_Syntax.command @{command_keyword print_translation}
  15.250 +  Outer_Syntax.command \<^command_keyword>\<open>print_translation\<close>
  15.251      "install print translation functions"
  15.252      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation));
  15.253  
  15.254  val _ =
  15.255 -  Outer_Syntax.command @{command_keyword typed_print_translation}
  15.256 +  Outer_Syntax.command \<^command_keyword>\<open>typed_print_translation\<close>
  15.257      "install typed print translation functions"
  15.258      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
  15.259  
  15.260  val _ =
  15.261 -  Outer_Syntax.command @{command_keyword print_ast_translation}
  15.262 +  Outer_Syntax.command \<^command_keyword>\<open>print_ast_translation\<close>
  15.263      "install print ast translation functions"
  15.264      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
  15.265  
  15.266 @@ -368,13 +368,13 @@
  15.267  local
  15.268  
  15.269  val _ =
  15.270 -  Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
  15.271 +  Outer_Syntax.local_theory' \<^command_keyword>\<open>definition\<close> "constant definition"
  15.272      (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
  15.273        Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) =>
  15.274          #2 oo Specification.definition_cmd decl params prems spec));
  15.275  
  15.276  val _ =
  15.277 -  Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
  15.278 +  Outer_Syntax.local_theory' \<^command_keyword>\<open>abbreviation\<close> "constant abbreviation"
  15.279      (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes
  15.280        >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec));
  15.281  
  15.282 @@ -383,19 +383,19 @@
  15.283    Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
  15.284  
  15.285  val _ =
  15.286 -  Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
  15.287 +  Outer_Syntax.command \<^command_keyword>\<open>axiomatization\<close> "axiomatic constant specification"
  15.288      (Scan.optional Parse.vars [] --
  15.289        Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
  15.290        >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
  15.291  
  15.292  val _ =
  15.293 -  Outer_Syntax.local_theory @{command_keyword alias} "name-space alias for constant"
  15.294 -    (Parse.binding -- (Parse.!!! @{keyword =} |-- Parse.position Parse.name)
  15.295 +  Outer_Syntax.local_theory \<^command_keyword>\<open>alias\<close> "name-space alias for constant"
  15.296 +    (Parse.binding -- (Parse.!!! \<^keyword>\<open>=\<close> |-- Parse.position Parse.name)
  15.297        >> Specification.alias_cmd);
  15.298  
  15.299  val _ =
  15.300 -  Outer_Syntax.local_theory @{command_keyword type_alias} "name-space alias for type constructor"
  15.301 -    (Parse.binding -- (Parse.!!! @{keyword =} |-- Parse.position Parse.name)
  15.302 +  Outer_Syntax.local_theory \<^command_keyword>\<open>type_alias\<close> "name-space alias for type constructor"
  15.303 +    (Parse.binding -- (Parse.!!! \<^keyword>\<open>=\<close> |-- Parse.position Parse.name)
  15.304        >> Specification.type_alias_cmd);
  15.305  
  15.306  in end\<close>
  15.307 @@ -407,25 +407,25 @@
  15.308  local
  15.309  
  15.310  val _ =
  15.311 -  Outer_Syntax.local_theory @{command_keyword type_notation}
  15.312 +  Outer_Syntax.local_theory \<^command_keyword>\<open>type_notation\<close>
  15.313      "add concrete syntax for type constructors"
  15.314      (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
  15.315        >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
  15.316  
  15.317  val _ =
  15.318 -  Outer_Syntax.local_theory @{command_keyword no_type_notation}
  15.319 +  Outer_Syntax.local_theory \<^command_keyword>\<open>no_type_notation\<close>
  15.320      "delete concrete syntax for type constructors"
  15.321      (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
  15.322        >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
  15.323  
  15.324  val _ =
  15.325 -  Outer_Syntax.local_theory @{command_keyword notation}
  15.326 +  Outer_Syntax.local_theory \<^command_keyword>\<open>notation\<close>
  15.327      "add concrete syntax for constants / fixed variables"
  15.328      (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
  15.329        >> (fn (mode, args) => Specification.notation_cmd true mode args));
  15.330  
  15.331  val _ =
  15.332 -  Outer_Syntax.local_theory @{command_keyword no_notation}
  15.333 +  Outer_Syntax.local_theory \<^command_keyword>\<open>no_notation\<close>
  15.334      "delete concrete syntax for constants / fixed variables"
  15.335      (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
  15.336        >> (fn (mode, args) => Specification.notation_cmd false mode args));
  15.337 @@ -459,11 +459,11 @@
  15.338        ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
  15.339          long Thm.theoremK NONE (K I) binding includes elems concl)));
  15.340  
  15.341 -val _ = theorem @{command_keyword theorem} false "theorem";
  15.342 -val _ = theorem @{command_keyword lemma} false "lemma";
  15.343 -val _ = theorem @{command_keyword corollary} false "corollary";
  15.344 -val _ = theorem @{command_keyword proposition} false "proposition";
  15.345 -val _ = theorem @{command_keyword schematic_goal} true "schematic goal";
  15.346 +val _ = theorem \<^command_keyword>\<open>theorem\<close> false "theorem";
  15.347 +val _ = theorem \<^command_keyword>\<open>lemma\<close> false "lemma";
  15.348 +val _ = theorem \<^command_keyword>\<open>corollary\<close> false "corollary";
  15.349 +val _ = theorem \<^command_keyword>\<open>proposition\<close> false "proposition";
  15.350 +val _ = theorem \<^command_keyword>\<open>schematic_goal\<close> true "schematic goal";
  15.351  
  15.352  in end\<close>
  15.353  
  15.354 @@ -471,18 +471,18 @@
  15.355  local
  15.356  
  15.357  val _ =
  15.358 -  Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
  15.359 +  Outer_Syntax.local_theory' \<^command_keyword>\<open>lemmas\<close> "define theorems"
  15.360      (Parse_Spec.name_facts -- Parse.for_fixes >>
  15.361        (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes));
  15.362  
  15.363  val _ =
  15.364 -  Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
  15.365 +  Outer_Syntax.local_theory' \<^command_keyword>\<open>declare\<close> "declare theorems"
  15.366      (Parse.and_list1 Parse.thms1 -- Parse.for_fixes
  15.367        >> (fn (facts, fixes) =>
  15.368            #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes));
  15.369  
  15.370  val _ =
  15.371 -  Outer_Syntax.local_theory @{command_keyword named_theorems}
  15.372 +  Outer_Syntax.local_theory \<^command_keyword>\<open>named_theorems\<close>
  15.373      "declare named collection of theorems"
  15.374      (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
  15.375        fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
  15.376 @@ -503,19 +503,19 @@
  15.377          in fold (hide fully o prep ctxt) args thy end))));
  15.378  
  15.379  val _ =
  15.380 -  hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class
  15.381 +  hide_names \<^command_keyword>\<open>hide_class\<close> "classes" Sign.hide_class Parse.class
  15.382      Proof_Context.read_class;
  15.383  
  15.384  val _ =
  15.385 -  hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const
  15.386 +  hide_names \<^command_keyword>\<open>hide_type\<close> "types" Sign.hide_type Parse.type_const
  15.387      ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
  15.388  
  15.389  val _ =
  15.390 -  hide_names @{command_keyword hide_const} "consts" Sign.hide_const Parse.const
  15.391 +  hide_names \<^command_keyword>\<open>hide_const\<close> "consts" Sign.hide_const Parse.const
  15.392      ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
  15.393  
  15.394  val _ =
  15.395 -  hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
  15.396 +  hide_names \<^command_keyword>\<open>hide_fact\<close> "facts" Global_Theory.hide_fact
  15.397      (Parse.position Parse.name) (Global_Theory.check_fact o Proof_Context.theory_of);
  15.398  
  15.399  in end\<close>
  15.400 @@ -527,29 +527,29 @@
  15.401  local
  15.402  
  15.403  val _ =
  15.404 -  Outer_Syntax.maybe_begin_local_theory @{command_keyword bundle}
  15.405 +  Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\<open>bundle\<close>
  15.406      "define bundle of declarations"
  15.407 -    ((Parse.binding --| @{keyword =}) -- Parse.thms1 -- Parse.for_fixes
  15.408 +    ((Parse.binding --| \<^keyword>\<open>=\<close>) -- Parse.thms1 -- Parse.for_fixes
  15.409        >> (uncurry Bundle.bundle_cmd))
  15.410      (Parse.binding --| Parse.begin >> Bundle.init);
  15.411  
  15.412  val _ =
  15.413 -  Outer_Syntax.local_theory @{command_keyword unbundle}
  15.414 +  Outer_Syntax.local_theory \<^command_keyword>\<open>unbundle\<close>
  15.415      "activate declarations from bundle in local theory"
  15.416      (Scan.repeat1 (Parse.position Parse.name) >> Bundle.unbundle_cmd);
  15.417  
  15.418  val _ =
  15.419 -  Outer_Syntax.command @{command_keyword include}
  15.420 +  Outer_Syntax.command \<^command_keyword>\<open>include\<close>
  15.421      "activate declarations from bundle in proof body"
  15.422      (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd));
  15.423  
  15.424  val _ =
  15.425 -  Outer_Syntax.command @{command_keyword including}
  15.426 +  Outer_Syntax.command \<^command_keyword>\<open>including\<close>
  15.427      "activate declarations from bundle in goal refinement"
  15.428      (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.including_cmd));
  15.429  
  15.430  val _ =
  15.431 -  Outer_Syntax.command @{command_keyword print_bundles}
  15.432 +  Outer_Syntax.command \<^command_keyword>\<open>print_bundles\<close>
  15.433      "print bundles of declarations"
  15.434      (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
  15.435  
  15.436 @@ -564,7 +564,7 @@
  15.437  local
  15.438  
  15.439  val _ =
  15.440 -  Outer_Syntax.command @{command_keyword context} "begin local theory context"
  15.441 +  Outer_Syntax.command \<^command_keyword>\<open>context\<close> "begin local theory context"
  15.442      ((Parse.position Parse.name >> (fn name =>
  15.443          Toplevel.begin_local_theory true (Named_Target.begin name)) ||
  15.444        Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
  15.445 @@ -572,7 +572,7 @@
  15.446        --| Parse.begin);
  15.447  
  15.448  val _ =
  15.449 -  Outer_Syntax.command @{command_keyword end} "end context"
  15.450 +  Outer_Syntax.command \<^command_keyword>\<open>end\<close> "end context"
  15.451      (Scan.succeed
  15.452        (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
  15.453          Toplevel.end_proof (K Proof.end_notepad)));
  15.454 @@ -587,19 +587,19 @@
  15.455  
  15.456  val locale_val =
  15.457    Parse_Spec.locale_expression --
  15.458 -    Scan.optional (@{keyword +} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
  15.459 +    Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
  15.460    Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
  15.461  
  15.462  val _ =
  15.463 -  Outer_Syntax.command @{command_keyword locale} "define named specification context"
  15.464 +  Outer_Syntax.command \<^command_keyword>\<open>locale\<close> "define named specification context"
  15.465      (Parse.binding --
  15.466 -      Scan.optional (@{keyword =} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
  15.467 +      Scan.optional (\<^keyword>\<open>=\<close> |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
  15.468        >> (fn ((name, (expr, elems)), begin) =>
  15.469            Toplevel.begin_local_theory begin
  15.470              (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
  15.471  
  15.472  val _ =
  15.473 -  Outer_Syntax.command @{command_keyword experiment} "open private specification context"
  15.474 +  Outer_Syntax.command \<^command_keyword>\<open>experiment\<close> "open private specification context"
  15.475      (Scan.repeat Parse_Spec.context_element --| Parse.begin
  15.476        >> (fn elems =>
  15.477            Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
  15.478 @@ -607,38 +607,38 @@
  15.479  val interpretation_args =
  15.480    Parse.!!! Parse_Spec.locale_expression --
  15.481      Scan.optional
  15.482 -      (@{keyword rewrites} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
  15.483 +      (\<^keyword>\<open>rewrites\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
  15.484  
  15.485  val _ =
  15.486 -  Outer_Syntax.command @{command_keyword interpret}
  15.487 +  Outer_Syntax.command \<^command_keyword>\<open>interpret\<close>
  15.488      "prove interpretation of locale expression in proof context"
  15.489      (interpretation_args >> (fn (expr, equations) =>
  15.490        Toplevel.proof (Interpretation.interpret_cmd expr equations)));
  15.491  
  15.492  val interpretation_args_with_defs =
  15.493    Parse.!!! Parse_Spec.locale_expression --
  15.494 -    (Scan.optional (@{keyword defines} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
  15.495 -      -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword =} -- Parse.term))) [] --
  15.496 +    (Scan.optional (\<^keyword>\<open>defines\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
  15.497 +      -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))) [] --
  15.498      Scan.optional
  15.499 -      (@{keyword rewrites} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
  15.500 +      (\<^keyword>\<open>rewrites\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
  15.501  
  15.502  val _ =
  15.503 -  Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation}
  15.504 +  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretation\<close>
  15.505      "prove interpretation of locale expression into global theory"
  15.506      (interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
  15.507        Interpretation.global_interpretation_cmd expr defs equations));
  15.508  
  15.509  val _ =
  15.510 -  Outer_Syntax.command @{command_keyword sublocale}
  15.511 +  Outer_Syntax.command \<^command_keyword>\<open>sublocale\<close>
  15.512      "prove sublocale relation between a locale and a locale expression"
  15.513 -    ((Parse.position Parse.name --| (@{keyword \<subseteq>} || @{keyword <}) --
  15.514 +    ((Parse.position Parse.name --| (\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) --
  15.515        interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) =>
  15.516          Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations)))
  15.517      || interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
  15.518          Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs equations)));
  15.519  
  15.520  val _ =
  15.521 -  Outer_Syntax.command @{command_keyword interpretation}
  15.522 +  Outer_Syntax.command \<^command_keyword>\<open>interpretation\<close>
  15.523      "prove interpretation of locale expression in local theory or into global theory"
  15.524      (interpretation_args >> (fn (expr, equations) =>
  15.525        Toplevel.local_theory_to_proof NONE NONE
  15.526 @@ -654,29 +654,29 @@
  15.527  
  15.528  val class_val =
  15.529    Parse_Spec.class_expression --
  15.530 -    Scan.optional (@{keyword +} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
  15.531 +    Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
  15.532    Scan.repeat1 Parse_Spec.context_element >> pair [];
  15.533  
  15.534  val _ =
  15.535 -  Outer_Syntax.command @{command_keyword class} "define type class"
  15.536 -   (Parse.binding -- Scan.optional (@{keyword =} |-- class_val) ([], []) -- Parse.opt_begin
  15.537 +  Outer_Syntax.command \<^command_keyword>\<open>class\<close> "define type class"
  15.538 +   (Parse.binding -- Scan.optional (\<^keyword>\<open>=\<close> |-- class_val) ([], []) -- Parse.opt_begin
  15.539      >> (fn ((name, (supclasses, elems)), begin) =>
  15.540          Toplevel.begin_local_theory begin
  15.541            (Class_Declaration.class_cmd name supclasses elems #> snd)));
  15.542  
  15.543  val _ =
  15.544 -  Outer_Syntax.local_theory_to_proof @{command_keyword subclass} "prove a subclass relation"
  15.545 +  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>subclass\<close> "prove a subclass relation"
  15.546      (Parse.class >> Class_Declaration.subclass_cmd);
  15.547  
  15.548  val _ =
  15.549 -  Outer_Syntax.command @{command_keyword instantiation} "instantiate and prove type arity"
  15.550 +  Outer_Syntax.command \<^command_keyword>\<open>instantiation\<close> "instantiate and prove type arity"
  15.551     (Parse.multi_arity --| Parse.begin
  15.552       >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
  15.553  
  15.554  val _ =
  15.555 -  Outer_Syntax.command @{command_keyword instance} "prove type arity or subclass relation"
  15.556 +  Outer_Syntax.command \<^command_keyword>\<open>instance\<close> "prove type arity or subclass relation"
  15.557    ((Parse.class --
  15.558 -    ((@{keyword \<subseteq>} || @{keyword <}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
  15.559 +    ((\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
  15.560      Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
  15.561      Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I)));
  15.562  
  15.563 @@ -689,9 +689,9 @@
  15.564  local
  15.565  
  15.566  val _ =
  15.567 -  Outer_Syntax.command @{command_keyword overloading} "overloaded definitions"
  15.568 -   (Scan.repeat1 (Parse.name --| (@{keyword ==} || @{keyword \<equiv>}) -- Parse.term --
  15.569 -      Scan.optional (@{keyword "("} |-- (@{keyword unchecked} >> K false) --| @{keyword ")"}) true
  15.570 +  Outer_Syntax.command \<^command_keyword>\<open>overloading\<close> "overloaded definitions"
  15.571 +   (Scan.repeat1 (Parse.name --| (\<^keyword>\<open>==\<close> || \<^keyword>\<open>\<equiv>\<close>) -- Parse.term --
  15.572 +      Scan.optional (\<^keyword>\<open>(\<close> |-- (\<^keyword>\<open>unchecked\<close> >> K false) --| \<^keyword>\<open>)\<close>) true
  15.573        >> Scan.triple1) --| Parse.begin
  15.574     >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
  15.575  
  15.576 @@ -704,7 +704,7 @@
  15.577  local
  15.578  
  15.579  val _ =
  15.580 -  Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
  15.581 +  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>notepad\<close> "begin proof context"
  15.582      (Parse.begin >> K Proof.begin_notepad);
  15.583  
  15.584  in end\<close>
  15.585 @@ -720,22 +720,22 @@
  15.586      >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
  15.587  
  15.588  val _ =
  15.589 -  Outer_Syntax.command @{command_keyword have} "state local goal"
  15.590 +  Outer_Syntax.command \<^command_keyword>\<open>have\<close> "state local goal"
  15.591      (structured_statement >> (fn (a, b, c, d) =>
  15.592        Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2)));
  15.593  
  15.594  val _ =
  15.595 -  Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals"
  15.596 +  Outer_Syntax.command \<^command_keyword>\<open>show\<close> "state local goal, to refine pending subgoals"
  15.597      (structured_statement >> (fn (a, b, c, d) =>
  15.598        Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2)));
  15.599  
  15.600  val _ =
  15.601 -  Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
  15.602 +  Outer_Syntax.command \<^command_keyword>\<open>hence\<close> "old-style alias of \"then have\""
  15.603      (structured_statement >> (fn (a, b, c, d) =>
  15.604        Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2)));
  15.605  
  15.606  val _ =
  15.607 -  Outer_Syntax.command @{command_keyword thus} "old-style alias of  \"then show\""
  15.608 +  Outer_Syntax.command \<^command_keyword>\<open>thus\<close> "old-style alias of  \"then show\""
  15.609      (structured_statement >> (fn (a, b, c, d) =>
  15.610        Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2)));
  15.611  
  15.612 @@ -750,31 +750,31 @@
  15.613  val facts = Parse.and_list1 Parse.thms1;
  15.614  
  15.615  val _ =
  15.616 -  Outer_Syntax.command @{command_keyword then} "forward chaining"
  15.617 +  Outer_Syntax.command \<^command_keyword>\<open>then\<close> "forward chaining"
  15.618      (Scan.succeed (Toplevel.proof Proof.chain));
  15.619  
  15.620  val _ =
  15.621 -  Outer_Syntax.command @{command_keyword from} "forward chaining from given facts"
  15.622 +  Outer_Syntax.command \<^command_keyword>\<open>from\<close> "forward chaining from given facts"
  15.623      (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
  15.624  
  15.625  val _ =
  15.626 -  Outer_Syntax.command @{command_keyword with} "forward chaining from given and current facts"
  15.627 +  Outer_Syntax.command \<^command_keyword>\<open>with\<close> "forward chaining from given and current facts"
  15.628      (facts >> (Toplevel.proof o Proof.with_thmss_cmd));
  15.629  
  15.630  val _ =
  15.631 -  Outer_Syntax.command @{command_keyword note} "define facts"
  15.632 +  Outer_Syntax.command \<^command_keyword>\<open>note\<close> "define facts"
  15.633      (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
  15.634  
  15.635  val _ =
  15.636 -  Outer_Syntax.command @{command_keyword supply} "define facts during goal refinement (unstructured)"
  15.637 +  Outer_Syntax.command \<^command_keyword>\<open>supply\<close> "define facts during goal refinement (unstructured)"
  15.638      (Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd));
  15.639  
  15.640  val _ =
  15.641 -  Outer_Syntax.command @{command_keyword using} "augment goal facts"
  15.642 +  Outer_Syntax.command \<^command_keyword>\<open>using\<close> "augment goal facts"
  15.643      (facts >> (Toplevel.proof o Proof.using_cmd));
  15.644  
  15.645  val _ =
  15.646 -  Outer_Syntax.command @{command_keyword unfolding} "unfold definitions in goal and facts"
  15.647 +  Outer_Syntax.command \<^command_keyword>\<open>unfolding\<close> "unfold definitions in goal and facts"
  15.648      (facts >> (Toplevel.proof o Proof.unfolding_cmd));
  15.649  
  15.650  in end\<close>
  15.651 @@ -790,51 +790,51 @@
  15.652      >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
  15.653  
  15.654  val _ =
  15.655 -  Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)"
  15.656 +  Outer_Syntax.command \<^command_keyword>\<open>fix\<close> "fix local variables (Skolem constants)"
  15.657      (Parse.vars >> (Toplevel.proof o Proof.fix_cmd));
  15.658  
  15.659  val _ =
  15.660 -  Outer_Syntax.command @{command_keyword assume} "assume propositions"
  15.661 +  Outer_Syntax.command \<^command_keyword>\<open>assume\<close> "assume propositions"
  15.662      (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c)));
  15.663  
  15.664  val _ =
  15.665 -  Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later"
  15.666 +  Outer_Syntax.command \<^command_keyword>\<open>presume\<close> "assume propositions, to be established later"
  15.667      (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
  15.668  
  15.669  val _ =
  15.670 -  Outer_Syntax.command @{command_keyword define} "local definition (non-polymorphic)"
  15.671 +  Outer_Syntax.command \<^command_keyword>\<open>define\<close> "local definition (non-polymorphic)"
  15.672      ((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
  15.673        >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
  15.674  
  15.675  val _ =
  15.676 -  Outer_Syntax.command @{command_keyword consider} "state cases rule"
  15.677 +  Outer_Syntax.command \<^command_keyword>\<open>consider\<close> "state cases rule"
  15.678      (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));
  15.679  
  15.680  val _ =
  15.681 -  Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
  15.682 +  Outer_Syntax.command \<^command_keyword>\<open>obtain\<close> "generalized elimination"
  15.683      (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement
  15.684        >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
  15.685  
  15.686  val _ =
  15.687 -  Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
  15.688 +  Outer_Syntax.command \<^command_keyword>\<open>guess\<close> "wild guessing (unstructured)"
  15.689      (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd));
  15.690  
  15.691  val _ =
  15.692 -  Outer_Syntax.command @{command_keyword let} "bind text variables"
  15.693 -    (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword =} |-- Parse.term))
  15.694 +  Outer_Syntax.command \<^command_keyword>\<open>let\<close> "bind text variables"
  15.695 +    (Parse.and_list1 (Parse.and_list1 Parse.term -- (\<^keyword>\<open>=\<close> |-- Parse.term))
  15.696        >> (Toplevel.proof o Proof.let_bind_cmd));
  15.697  
  15.698  val _ =
  15.699 -  Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables"
  15.700 +  Outer_Syntax.command \<^command_keyword>\<open>write\<close> "add concrete syntax for constants / fixed variables"
  15.701      (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
  15.702      >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
  15.703  
  15.704  val _ =
  15.705 -  Outer_Syntax.command @{command_keyword case} "invoke local context"
  15.706 +  Outer_Syntax.command \<^command_keyword>\<open>case\<close> "invoke local context"
  15.707      (Parse_Spec.opt_thm_name ":" --
  15.708 -      (@{keyword "("} |--
  15.709 +      (\<^keyword>\<open>(\<close> |--
  15.710          Parse.!!! (Parse.position Parse.name -- Scan.repeat (Parse.maybe Parse.binding)
  15.711 -          --| @{keyword ")"}) ||
  15.712 +          --| \<^keyword>\<open>)\<close>) ||
  15.713          Parse.position Parse.name >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
  15.714  
  15.715  in end\<close>
  15.716 @@ -846,15 +846,15 @@
  15.717  local
  15.718  
  15.719  val _ =
  15.720 -  Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block"
  15.721 +  Outer_Syntax.command \<^command_keyword>\<open>{\<close> "begin explicit proof block"
  15.722      (Scan.succeed (Toplevel.proof Proof.begin_block));
  15.723  
  15.724  val _ =
  15.725 -  Outer_Syntax.command @{command_keyword "}"} "end explicit proof block"
  15.726 +  Outer_Syntax.command \<^command_keyword>\<open>}\<close> "end explicit proof block"
  15.727      (Scan.succeed (Toplevel.proof Proof.end_block));
  15.728  
  15.729  val _ =
  15.730 -  Outer_Syntax.command @{command_keyword next} "enter next proof block"
  15.731 +  Outer_Syntax.command \<^command_keyword>\<open>next\<close> "enter next proof block"
  15.732      (Scan.succeed (Toplevel.proof Proof.next_block));
  15.733  
  15.734  in end\<close>
  15.735 @@ -866,40 +866,40 @@
  15.736  local
  15.737  
  15.738  val _ =
  15.739 -  Outer_Syntax.command @{command_keyword qed} "conclude proof"
  15.740 +  Outer_Syntax.command \<^command_keyword>\<open>qed\<close> "conclude proof"
  15.741      (Scan.option Method.parse >> (fn m =>
  15.742       (Option.map Method.report m;
  15.743        Isar_Cmd.qed m)));
  15.744  
  15.745  val _ =
  15.746 -  Outer_Syntax.command @{command_keyword by} "terminal backward proof"
  15.747 +  Outer_Syntax.command \<^command_keyword>\<open>by\<close> "terminal backward proof"
  15.748      (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
  15.749       (Method.report m1;
  15.750        Option.map Method.report m2;
  15.751        Isar_Cmd.terminal_proof (m1, m2))));
  15.752  
  15.753  val _ =
  15.754 -  Outer_Syntax.command @{command_keyword ".."} "default proof"
  15.755 +  Outer_Syntax.command \<^command_keyword>\<open>..\<close> "default proof"
  15.756      (Scan.succeed Isar_Cmd.default_proof);
  15.757  
  15.758  val _ =
  15.759 -  Outer_Syntax.command @{command_keyword "."} "immediate proof"
  15.760 +  Outer_Syntax.command \<^command_keyword>\<open>.\<close> "immediate proof"
  15.761      (Scan.succeed Isar_Cmd.immediate_proof);
  15.762  
  15.763  val _ =
  15.764 -  Outer_Syntax.command @{command_keyword done} "done proof"
  15.765 +  Outer_Syntax.command \<^command_keyword>\<open>done\<close> "done proof"
  15.766      (Scan.succeed Isar_Cmd.done_proof);
  15.767  
  15.768  val _ =
  15.769 -  Outer_Syntax.command @{command_keyword sorry} "skip proof (quick-and-dirty mode only!)"
  15.770 +  Outer_Syntax.command \<^command_keyword>\<open>sorry\<close> "skip proof (quick-and-dirty mode only!)"
  15.771      (Scan.succeed Isar_Cmd.skip_proof);
  15.772  
  15.773  val _ =
  15.774 -  Outer_Syntax.command @{command_keyword \<proof>} "dummy proof (quick-and-dirty mode only!)"
  15.775 +  Outer_Syntax.command \<^command_keyword>\<open>\<proof>\<close> "dummy proof (quick-and-dirty mode only!)"
  15.776      (Scan.succeed Isar_Cmd.skip_proof);
  15.777  
  15.778  val _ =
  15.779 -  Outer_Syntax.command @{command_keyword oops} "forget proof"
  15.780 +  Outer_Syntax.command \<^command_keyword>\<open>oops\<close> "forget proof"
  15.781      (Scan.succeed (Toplevel.forget_proof true));
  15.782  
  15.783  in end\<close>
  15.784 @@ -911,23 +911,23 @@
  15.785  local
  15.786  
  15.787  val _ =
  15.788 -  Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state"
  15.789 +  Outer_Syntax.command \<^command_keyword>\<open>defer\<close> "shuffle internal proof state"
  15.790      (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
  15.791  
  15.792  val _ =
  15.793 -  Outer_Syntax.command @{command_keyword prefer} "shuffle internal proof state"
  15.794 +  Outer_Syntax.command \<^command_keyword>\<open>prefer\<close> "shuffle internal proof state"
  15.795      (Parse.nat >> (Toplevel.proof o Proof.prefer));
  15.796  
  15.797  val _ =
  15.798 -  Outer_Syntax.command @{command_keyword apply} "initial goal refinement step (unstructured)"
  15.799 +  Outer_Syntax.command \<^command_keyword>\<open>apply\<close> "initial goal refinement step (unstructured)"
  15.800      (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m))));
  15.801  
  15.802  val _ =
  15.803 -  Outer_Syntax.command @{command_keyword apply_end} "terminal goal refinement step (unstructured)"
  15.804 +  Outer_Syntax.command \<^command_keyword>\<open>apply_end\<close> "terminal goal refinement step (unstructured)"
  15.805      (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m))));
  15.806  
  15.807  val _ =
  15.808 -  Outer_Syntax.command @{command_keyword proof} "backward proof step"
  15.809 +  Outer_Syntax.command \<^command_keyword>\<open>proof\<close> "backward proof step"
  15.810      (Scan.option Method.parse >> (fn m =>
  15.811        (Option.map Method.report m;
  15.812         Toplevel.proof (fn state =>
  15.813 @@ -952,15 +952,15 @@
  15.814  
  15.815  val for_params =
  15.816    Scan.optional
  15.817 -    (@{keyword for} |--
  15.818 +    (\<^keyword>\<open>for\<close> |--
  15.819        Parse.!!! ((Scan.option Parse.dots >> is_some) --
  15.820          (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
  15.821      (false, []);
  15.822  
  15.823  val _ =
  15.824 -  Outer_Syntax.command @{command_keyword subgoal}
  15.825 +  Outer_Syntax.command \<^command_keyword>\<open>subgoal\<close>
  15.826      "focus on first subgoal within backward refinement"
  15.827 -    (opt_fact_binding -- (Scan.option (@{keyword premises} |-- Parse.!!! opt_fact_binding)) --
  15.828 +    (opt_fact_binding -- (Scan.option (\<^keyword>\<open>premises\<close> |-- Parse.!!! opt_fact_binding)) --
  15.829        for_params >> (fn ((a, b), c) =>
  15.830          Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
  15.831  
  15.832 @@ -973,28 +973,28 @@
  15.833  local
  15.834  
  15.835  val calculation_args =
  15.836 -  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.thms1 --| @{keyword ")"})));
  15.837 +  Scan.option (\<^keyword>\<open>(\<close> |-- Parse.!!! ((Parse.thms1 --| \<^keyword>\<open>)\<close>)));
  15.838  
  15.839  val _ =
  15.840 -  Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
  15.841 +  Outer_Syntax.command \<^command_keyword>\<open>also\<close> "combine calculation and current facts"
  15.842      (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd));
  15.843  
  15.844  val _ =
  15.845 -  Outer_Syntax.command @{command_keyword finally}
  15.846 +  Outer_Syntax.command \<^command_keyword>\<open>finally\<close>
  15.847      "combine calculation and current facts, exhibit result"
  15.848      (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd));
  15.849  
  15.850  val _ =
  15.851 -  Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts"
  15.852 +  Outer_Syntax.command \<^command_keyword>\<open>moreover\<close> "augment calculation by current facts"
  15.853      (Scan.succeed (Toplevel.proof' Calculation.moreover));
  15.854  
  15.855  val _ =
  15.856 -  Outer_Syntax.command @{command_keyword ultimately}
  15.857 +  Outer_Syntax.command \<^command_keyword>\<open>ultimately\<close>
  15.858      "augment calculation by current facts, exhibit result"
  15.859      (Scan.succeed (Toplevel.proof' Calculation.ultimately));
  15.860  
  15.861  val _ =
  15.862 -  Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
  15.863 +  Outer_Syntax.command \<^command_keyword>\<open>print_trans_rules\<close> "print transitivity rules"
  15.864      (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
  15.865  
  15.866  in end\<close>
  15.867 @@ -1009,7 +1009,7 @@
  15.868    Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"];
  15.869  
  15.870  val _ =
  15.871 -  Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
  15.872 +  Outer_Syntax.command \<^command_keyword>\<open>back\<close> "explicit backtracking of proof command"
  15.873      (Scan.succeed
  15.874       (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
  15.875        Toplevel.skip_proof report_back));
  15.876 @@ -1023,123 +1023,123 @@
  15.877  local
  15.878  
  15.879  val opt_modes =
  15.880 -  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
  15.881 +  Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\<open>)\<close>)) [];
  15.882  
  15.883  val _ =
  15.884 -  Outer_Syntax.command @{command_keyword help}
  15.885 +  Outer_Syntax.command \<^command_keyword>\<open>help\<close>
  15.886      "retrieve outer syntax commands according to name patterns"
  15.887      (Scan.repeat Parse.name >>
  15.888        (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats)));
  15.889  
  15.890  val _ =
  15.891 -  Outer_Syntax.command @{command_keyword print_commands} "print outer syntax commands"
  15.892 +  Outer_Syntax.command \<^command_keyword>\<open>print_commands\<close> "print outer syntax commands"
  15.893      (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of)));
  15.894  
  15.895  val _ =
  15.896 -  Outer_Syntax.command @{command_keyword print_options} "print configuration options"
  15.897 +  Outer_Syntax.command \<^command_keyword>\<open>print_options\<close> "print configuration options"
  15.898      (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
  15.899  
  15.900  val _ =
  15.901 -  Outer_Syntax.command @{command_keyword print_context}
  15.902 +  Outer_Syntax.command \<^command_keyword>\<open>print_context\<close>
  15.903      "print context of local theory target"
  15.904      (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
  15.905  
  15.906  val _ =
  15.907 -  Outer_Syntax.command @{command_keyword print_theory}
  15.908 +  Outer_Syntax.command \<^command_keyword>\<open>print_theory\<close>
  15.909      "print logical theory contents"
  15.910      (Parse.opt_bang >> (fn b =>
  15.911        Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of)));
  15.912  
  15.913  val _ =
  15.914 -  Outer_Syntax.command @{command_keyword print_definitions}
  15.915 +  Outer_Syntax.command \<^command_keyword>\<open>print_definitions\<close>
  15.916      "print dependencies of definitional theory content"
  15.917      (Parse.opt_bang >> (fn b =>
  15.918        Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of)));
  15.919  
  15.920  val _ =
  15.921 -  Outer_Syntax.command @{command_keyword print_syntax}
  15.922 +  Outer_Syntax.command \<^command_keyword>\<open>print_syntax\<close>
  15.923      "print inner syntax of context"
  15.924      (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
  15.925  
  15.926  val _ =
  15.927 -  Outer_Syntax.command @{command_keyword print_defn_rules}
  15.928 +  Outer_Syntax.command \<^command_keyword>\<open>print_defn_rules\<close>
  15.929      "print definitional rewrite rules of context"
  15.930      (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
  15.931  
  15.932  val _ =
  15.933 -  Outer_Syntax.command @{command_keyword print_abbrevs}
  15.934 +  Outer_Syntax.command \<^command_keyword>\<open>print_abbrevs\<close>
  15.935      "print constant abbreviations of context"
  15.936      (Parse.opt_bang >> (fn b =>
  15.937        Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
  15.938  
  15.939  val _ =
  15.940 -  Outer_Syntax.command @{command_keyword print_theorems}
  15.941 +  Outer_Syntax.command \<^command_keyword>\<open>print_theorems\<close>
  15.942      "print theorems of local theory or proof context"
  15.943      (Parse.opt_bang >> (fn b =>
  15.944        Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
  15.945  
  15.946  val _ =
  15.947 -  Outer_Syntax.command @{command_keyword print_locales}
  15.948 +  Outer_Syntax.command \<^command_keyword>\<open>print_locales\<close>
  15.949      "print locales of this theory"
  15.950      (Parse.opt_bang >> (fn b =>
  15.951        Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
  15.952  
  15.953  val _ =
  15.954 -  Outer_Syntax.command @{command_keyword print_classes}
  15.955 +  Outer_Syntax.command \<^command_keyword>\<open>print_classes\<close>
  15.956      "print classes of this theory"
  15.957      (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of)));
  15.958  
  15.959  val _ =
  15.960 -  Outer_Syntax.command @{command_keyword print_locale}
  15.961 +  Outer_Syntax.command \<^command_keyword>\<open>print_locale\<close>
  15.962      "print locale of this theory"
  15.963      (Parse.opt_bang -- Parse.position Parse.name >> (fn (b, name) =>
  15.964        Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
  15.965  
  15.966  val _ =
  15.967 -  Outer_Syntax.command @{command_keyword print_interps}
  15.968 +  Outer_Syntax.command \<^command_keyword>\<open>print_interps\<close>
  15.969      "print interpretations of locale for this theory or proof context"
  15.970      (Parse.position Parse.name >> (fn name =>
  15.971        Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
  15.972  
  15.973  val _ =
  15.974 -  Outer_Syntax.command @{command_keyword print_dependencies}
  15.975 +  Outer_Syntax.command \<^command_keyword>\<open>print_dependencies\<close>
  15.976      "print dependencies of locale expression"
  15.977      (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (b, expr) =>
  15.978        Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
  15.979  
  15.980  val _ =
  15.981 -  Outer_Syntax.command @{command_keyword print_attributes}
  15.982 +  Outer_Syntax.command \<^command_keyword>\<open>print_attributes\<close>
  15.983      "print attributes of this theory"
  15.984      (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
  15.985  
  15.986  val _ =
  15.987 -  Outer_Syntax.command @{command_keyword print_simpset}
  15.988 +  Outer_Syntax.command \<^command_keyword>\<open>print_simpset\<close>
  15.989      "print context of Simplifier"
  15.990      (Parse.opt_bang >> (fn b =>
  15.991        Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
  15.992  
  15.993  val _ =
  15.994 -  Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules"
  15.995 +  Outer_Syntax.command \<^command_keyword>\<open>print_rules\<close> "print intro/elim rules"
  15.996      (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
  15.997  
  15.998  val _ =
  15.999 -  Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory"
 15.1000 +  Outer_Syntax.command \<^command_keyword>\<open>print_methods\<close> "print methods of this theory"
 15.1001      (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
 15.1002  
 15.1003  val _ =
 15.1004 -  Outer_Syntax.command @{command_keyword print_antiquotations}
 15.1005 +  Outer_Syntax.command \<^command_keyword>\<open>print_antiquotations\<close>
 15.1006      "print document antiquotations"
 15.1007      (Parse.opt_bang >> (fn b =>
 15.1008        Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
 15.1009  
 15.1010  val _ =
 15.1011 -  Outer_Syntax.command @{command_keyword print_ML_antiquotations}
 15.1012 +  Outer_Syntax.command \<^command_keyword>\<open>print_ML_antiquotations\<close>
 15.1013      "print ML antiquotations"
 15.1014      (Parse.opt_bang >> (fn b =>
 15.1015        Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
 15.1016  
 15.1017  val _ =
 15.1018 -  Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
 15.1019 +  Outer_Syntax.command \<^command_keyword>\<open>locale_deps\<close> "visualize locale dependencies"
 15.1020      (Scan.succeed
 15.1021        (Toplevel.keep (Toplevel.theory_of #> (fn thy =>
 15.1022          Locale.pretty_locale_deps thy
 15.1023 @@ -1148,68 +1148,68 @@
 15.1024          |> Graph_Display.display_graph_old))));
 15.1025  
 15.1026  val _ =
 15.1027 -  Outer_Syntax.command @{command_keyword print_term_bindings}
 15.1028 +  Outer_Syntax.command \<^command_keyword>\<open>print_term_bindings\<close>
 15.1029      "print term bindings of proof context"
 15.1030      (Scan.succeed
 15.1031        (Toplevel.keep
 15.1032          (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
 15.1033  
 15.1034  val _ =
 15.1035 -  Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context"
 15.1036 +  Outer_Syntax.command \<^command_keyword>\<open>print_facts\<close> "print facts of proof context"
 15.1037      (Parse.opt_bang >> (fn b =>
 15.1038        Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
 15.1039  
 15.1040  val _ =
 15.1041 -  Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context"
 15.1042 +  Outer_Syntax.command \<^command_keyword>\<open>print_cases\<close> "print cases of proof context"
 15.1043      (Scan.succeed
 15.1044        (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
 15.1045  
 15.1046  val _ =
 15.1047 -  Outer_Syntax.command @{command_keyword print_statement}
 15.1048 +  Outer_Syntax.command \<^command_keyword>\<open>print_statement\<close>
 15.1049      "print theorems as long statements"
 15.1050      (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts);
 15.1051  
 15.1052  val _ =
 15.1053 -  Outer_Syntax.command @{command_keyword thm} "print theorems"
 15.1054 +  Outer_Syntax.command \<^command_keyword>\<open>thm\<close> "print theorems"
 15.1055      (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms);
 15.1056  
 15.1057  val _ =
 15.1058 -  Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
 15.1059 +  Outer_Syntax.command \<^command_keyword>\<open>prf\<close> "print proof terms of theorems"
 15.1060      (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false);
 15.1061  
 15.1062  val _ =
 15.1063 -  Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
 15.1064 +  Outer_Syntax.command \<^command_keyword>\<open>full_prf\<close> "print full proof terms of theorems"
 15.1065      (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true);
 15.1066  
 15.1067  val _ =
 15.1068 -  Outer_Syntax.command @{command_keyword prop} "read and print proposition"
 15.1069 +  Outer_Syntax.command \<^command_keyword>\<open>prop\<close> "read and print proposition"
 15.1070      (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
 15.1071  
 15.1072  val _ =
 15.1073 -  Outer_Syntax.command @{command_keyword term} "read and print term"
 15.1074 +  Outer_Syntax.command \<^command_keyword>\<open>term\<close> "read and print term"
 15.1075      (opt_modes -- Parse.term >> Isar_Cmd.print_term);
 15.1076  
 15.1077  val _ =
 15.1078 -  Outer_Syntax.command @{command_keyword typ} "read and print type"
 15.1079 -    (opt_modes -- (Parse.typ -- Scan.option (@{keyword ::} |-- Parse.!!! Parse.sort))
 15.1080 +  Outer_Syntax.command \<^command_keyword>\<open>typ\<close> "read and print type"
 15.1081 +    (opt_modes -- (Parse.typ -- Scan.option (\<^keyword>\<open>::\<close> |-- Parse.!!! Parse.sort))
 15.1082        >> Isar_Cmd.print_type);
 15.1083  
 15.1084  val _ =
 15.1085 -  Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
 15.1086 +  Outer_Syntax.command \<^command_keyword>\<open>print_codesetup\<close> "print code generator setup"
 15.1087      (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
 15.1088  
 15.1089  val _ =
 15.1090 -  Outer_Syntax.command @{command_keyword print_state}
 15.1091 +  Outer_Syntax.command \<^command_keyword>\<open>print_state\<close>
 15.1092      "print current proof state (if present)"
 15.1093      (opt_modes >> (fn modes =>
 15.1094        Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state))));
 15.1095  
 15.1096  val _ =
 15.1097 -  Outer_Syntax.command @{command_keyword welcome} "print welcome message"
 15.1098 +  Outer_Syntax.command \<^command_keyword>\<open>welcome\<close> "print welcome message"
 15.1099      (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ()))));
 15.1100  
 15.1101  val _ =
 15.1102 -  Outer_Syntax.command @{command_keyword display_drafts}
 15.1103 +  Outer_Syntax.command \<^command_keyword>\<open>display_drafts\<close>
 15.1104      "display raw source files with symbols"
 15.1105      (Scan.repeat1 Parse.path >> (fn names =>
 15.1106        Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
 15.1107 @@ -1224,26 +1224,26 @@
 15.1108  
 15.1109  val theory_bounds =
 15.1110    Parse.position Parse.theory_name >> single ||
 15.1111 -  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_name) --| @{keyword ")"});
 15.1112 +  (\<^keyword>\<open>(\<close> |-- Parse.enum "|" (Parse.position Parse.theory_name) --| \<^keyword>\<open>)\<close>);
 15.1113  
 15.1114  val _ =
 15.1115 -  Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
 15.1116 +  Outer_Syntax.command \<^command_keyword>\<open>thy_deps\<close> "visualize theory dependencies"
 15.1117      (Scan.option theory_bounds -- Scan.option theory_bounds >>
 15.1118        (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args)));
 15.1119  
 15.1120  
 15.1121  val class_bounds =
 15.1122    Parse.sort >> single ||
 15.1123 -  (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
 15.1124 +  (\<^keyword>\<open>(\<close> |-- Parse.enum "|" Parse.sort --| \<^keyword>\<open>)\<close>);
 15.1125  
 15.1126  val _ =
 15.1127 -  Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
 15.1128 +  Outer_Syntax.command \<^command_keyword>\<open>class_deps\<close> "visualize class dependencies"
 15.1129      (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
 15.1130        Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args)));
 15.1131  
 15.1132  
 15.1133  val _ =
 15.1134 -  Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
 15.1135 +  Outer_Syntax.command \<^command_keyword>\<open>thm_deps\<close> "visualize theorem dependencies"
 15.1136      (Parse.thms1 >> (fn args =>
 15.1137        Toplevel.keep (fn st =>
 15.1138          Thm_Deps.thm_deps (Toplevel.theory_of st)
 15.1139 @@ -1254,7 +1254,7 @@
 15.1140    Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name));
 15.1141  
 15.1142  val _ =
 15.1143 -  Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
 15.1144 +  Outer_Syntax.command \<^command_keyword>\<open>unused_thms\<close> "find unused theorems"
 15.1145      (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
 15.1146          Toplevel.keep (fn st =>
 15.1147            let
 15.1148 @@ -1280,7 +1280,7 @@
 15.1149  local
 15.1150  
 15.1151  val _ =
 15.1152 -  Outer_Syntax.command @{command_keyword find_consts}
 15.1153 +  Outer_Syntax.command \<^command_keyword>\<open>find_consts\<close>
 15.1154      "find constants by name / type patterns"
 15.1155      (Find_Consts.query_parser >> (fn spec =>
 15.1156        Toplevel.keep (fn st =>
 15.1157 @@ -1294,7 +1294,7 @@
 15.1158      (NONE, true);
 15.1159  
 15.1160  val _ =
 15.1161 -  Outer_Syntax.command @{command_keyword find_theorems}
 15.1162 +  Outer_Syntax.command \<^command_keyword>\<open>find_theorems\<close>
 15.1163      "find theorems meeting specified criteria"
 15.1164      (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) =>
 15.1165        Toplevel.keep (fn st =>
 15.1166 @@ -1310,7 +1310,7 @@
 15.1167  local
 15.1168  
 15.1169  val _ =
 15.1170 -  Outer_Syntax.command @{command_keyword code_datatype}
 15.1171 +  Outer_Syntax.command \<^command_keyword>\<open>code_datatype\<close>
 15.1172      "define set of code datatype constructors"
 15.1173      (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd));
 15.1174  
 15.1175 @@ -1325,24 +1325,24 @@
 15.1176  val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
 15.1177  
 15.1178  val _ =
 15.1179 -  Outer_Syntax.command @{command_keyword realizers}
 15.1180 +  Outer_Syntax.command \<^command_keyword>\<open>realizers\<close>
 15.1181      "specify realizers for primitive axioms / theorems, together with correctness proof"
 15.1182      (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
 15.1183       (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
 15.1184         (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
 15.1185  
 15.1186  val _ =
 15.1187 -  Outer_Syntax.command @{command_keyword realizability}
 15.1188 +  Outer_Syntax.command \<^command_keyword>\<open>realizability\<close>
 15.1189      "add equations characterizing realizability"
 15.1190      (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
 15.1191  
 15.1192  val _ =
 15.1193 -  Outer_Syntax.command @{command_keyword extract_type}
 15.1194 +  Outer_Syntax.command \<^command_keyword>\<open>extract_type\<close>
 15.1195      "add equations characterizing type of extracted program"
 15.1196      (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
 15.1197  
 15.1198  val _ =
 15.1199 -  Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
 15.1200 +  Outer_Syntax.command \<^command_keyword>\<open>extract\<close> "extract terms from proofs"
 15.1201      (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
 15.1202        Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
 15.1203  
    16.1 --- a/src/Pure/Thy/document_antiquotations.ML	Wed Dec 06 15:46:35 2017 +0100
    16.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Wed Dec 06 18:59:33 2017 +0100
    16.3 @@ -21,9 +21,9 @@
    16.4  
    16.5  val _ =
    16.6    Theory.setup
    16.7 -   (markdown_error @{binding item} #>
    16.8 -    markdown_error @{binding enum} #>
    16.9 -    markdown_error @{binding descr});
   16.10 +   (markdown_error \<^binding>\<open>item\<close> #>
   16.11 +    markdown_error \<^binding>\<open>enum\<close> #>
   16.12 +    markdown_error \<^binding>\<open>descr\<close>);
   16.13  
   16.14  end;
   16.15  
   16.16 @@ -32,10 +32,10 @@
   16.17  
   16.18  val _ =
   16.19    Theory.setup
   16.20 -   (Thy_Output.antiquotation @{binding noindent} (Scan.succeed ()) (K (K "\\noindent")) #>
   16.21 -    Thy_Output.antiquotation @{binding smallskip} (Scan.succeed ()) (K (K "\\smallskip")) #>
   16.22 -    Thy_Output.antiquotation @{binding medskip} (Scan.succeed ()) (K (K "\\medskip")) #>
   16.23 -    Thy_Output.antiquotation @{binding bigskip} (Scan.succeed ()) (K (K "\\bigskip")));
   16.24 +   (Thy_Output.antiquotation \<^binding>\<open>noindent\<close> (Scan.succeed ()) (K (K "\\noindent")) #>
   16.25 +    Thy_Output.antiquotation \<^binding>\<open>smallskip\<close> (Scan.succeed ()) (K (K "\\smallskip")) #>
   16.26 +    Thy_Output.antiquotation \<^binding>\<open>medskip\<close> (Scan.succeed ()) (K (K "\\medskip")) #>
   16.27 +    Thy_Output.antiquotation \<^binding>\<open>bigskip\<close> (Scan.succeed ()) (K (K "\\bigskip")));
   16.28  
   16.29  
   16.30  (* control style *)
   16.31 @@ -50,9 +50,9 @@
   16.32  
   16.33  val _ =
   16.34    Theory.setup
   16.35 -   (control_antiquotation @{binding footnote} "\\footnote{" "}" #>
   16.36 -    control_antiquotation @{binding emph} "\\emph{" "}" #>
   16.37 -    control_antiquotation @{binding bold} "\\textbf{" "}");
   16.38 +   (control_antiquotation \<^binding>\<open>footnote\<close> "\\footnote{" "}" #>
   16.39 +    control_antiquotation \<^binding>\<open>emph\<close> "\\emph{" "}" #>
   16.40 +    control_antiquotation \<^binding>\<open>bold\<close> "\\textbf{" "}");
   16.41  
   16.42  end;
   16.43  
   16.44 @@ -72,8 +72,8 @@
   16.45  
   16.46  val _ =
   16.47    Theory.setup
   16.48 -   (text_antiquotation @{binding text} #>
   16.49 -    text_antiquotation @{binding cartouche});
   16.50 +   (text_antiquotation \<^binding>\<open>text\<close> #>
   16.51 +    text_antiquotation \<^binding>\<open>cartouche\<close>);
   16.52  
   16.53  end;
   16.54  
   16.55 @@ -82,7 +82,7 @@
   16.56  
   16.57  val _ =
   16.58    Theory.setup
   16.59 -    (Thy_Output.antiquotation @{binding theory_text} (Scan.lift Args.text_input)
   16.60 +    (Thy_Output.antiquotation \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
   16.61        (fn {context = ctxt, ...} => fn source =>
   16.62          let
   16.63            val _ =
   16.64 @@ -122,8 +122,8 @@
   16.65  in
   16.66  
   16.67  val _ = Theory.setup
   16.68 - (goal_state @{binding goals} true #>
   16.69 -  goal_state @{binding subgoals} false);
   16.70 + (goal_state \<^binding>\<open>goals\<close> true #>
   16.71 +  goal_state \<^binding>\<open>subgoals\<close> false);
   16.72  
   16.73  end;
   16.74  
   16.75 @@ -131,7 +131,7 @@
   16.76  (* embedded lemma *)
   16.77  
   16.78  val _ = Theory.setup
   16.79 -  (Thy_Output.antiquotation @{binding lemma}
   16.80 +  (Thy_Output.antiquotation \<^binding>\<open>lemma\<close>
   16.81      (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
   16.82        Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
   16.83      (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
   16.84 @@ -156,7 +156,7 @@
   16.85  
   16.86  val _ =
   16.87    Theory.setup
   16.88 -    (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.text_input)
   16.89 +    (Thy_Output.antiquotation \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
   16.90        (fn {context = ctxt, ...} => fn source =>
   16.91         (Context_Position.report ctxt (Input.pos_of source)
   16.92            (Markup.language_verbatim (Input.is_delimited source));
   16.93 @@ -178,18 +178,18 @@
   16.94  in
   16.95  
   16.96  val _ = Theory.setup
   16.97 - (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>
   16.98 -  ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #>
   16.99 -  ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #>
  16.100 -  ml_text @{binding ML_structure}
  16.101 + (ml_text \<^binding>\<open>ML\<close> (ml_enclose "fn _ => (" ");") #>
  16.102 +  ml_text \<^binding>\<open>ML_op\<close> (ml_enclose "fn _ => (op " ");") #>
  16.103 +  ml_text \<^binding>\<open>ML_type\<close> (ml_enclose "val _ = NONE : (" ") option;") #>
  16.104 +  ml_text \<^binding>\<open>ML_structure\<close>
  16.105      (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
  16.106  
  16.107 -  ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
  16.108 +  ml_text \<^binding>\<open>ML_functor\<close>   (* FIXME formal treatment of functor name (!?) *)
  16.109      (fn source =>
  16.110        ML_Lex.read ("ML_Env.check_functor " ^
  16.111          ML_Syntax.print_string (Input.source_content source))) #>
  16.112  
  16.113 -  ml_text @{binding ML_text} (K []));
  16.114 +  ml_text \<^binding>\<open>ML_text\<close> (K []));
  16.115  
  16.116  end;
  16.117  
  16.118 @@ -197,7 +197,7 @@
  16.119  (* URLs *)
  16.120  
  16.121  val _ = Theory.setup
  16.122 -  (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.embedded))
  16.123 +  (Thy_Output.antiquotation \<^binding>\<open>url\<close> (Scan.lift (Parse.position Parse.embedded))
  16.124      (fn {context = ctxt, ...} => fn (name, pos) =>
  16.125        (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
  16.126         enclose "\\url{" "}" name)));
  16.127 @@ -206,7 +206,7 @@
  16.128  (* doc entries *)
  16.129  
  16.130  val _ = Theory.setup
  16.131 -  (Thy_Output.antiquotation @{binding doc} (Scan.lift (Parse.position Parse.embedded))
  16.132 +  (Thy_Output.antiquotation \<^binding>\<open>doc\<close> (Scan.lift (Parse.position Parse.embedded))
  16.133      (fn {context = ctxt, ...} => fn (name, pos) =>
  16.134        (Context_Position.report ctxt pos (Markup.doc name);
  16.135          Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name])));
  16.136 @@ -220,11 +220,11 @@
  16.137  
  16.138  val _ =
  16.139    Theory.setup
  16.140 -   (entity_antiquotation @{binding command} Outer_Syntax.check_command
  16.141 +   (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command
  16.142       (enclose "\\isacommand{" "}" o Output.output) #>
  16.143 -    entity_antiquotation @{binding method} Method.check_name
  16.144 +    entity_antiquotation \<^binding>\<open>method\<close> Method.check_name
  16.145       (enclose "\\isa{" "}" o Output.output) #>
  16.146 -    entity_antiquotation @{binding attribute} Attrib.check_name
  16.147 +    entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name
  16.148       (enclose "\\isa{" "}" o Output.output));
  16.149  
  16.150  end;
    17.1 --- a/src/Pure/Thy/term_style.ML	Wed Dec 06 15:46:35 2017 +0100
    17.2 +++ b/src/Pure/Thy/term_style.ML	Wed Dec 06 18:59:33 2017 +0100
    17.3 @@ -82,10 +82,10 @@
    17.4    | sub_term t = t;
    17.5  
    17.6  val _ = Theory.setup
    17.7 - (setup @{binding lhs} (style_lhs_rhs fst) #>
    17.8 -  setup @{binding rhs} (style_lhs_rhs snd) #>
    17.9 -  setup @{binding prem} style_prem #>
   17.10 -  setup @{binding concl} (Scan.succeed (K Logic.strip_imp_concl)) #>
   17.11 -  setup @{binding sub} (Scan.succeed (K sub_term)));
   17.12 + (setup \<^binding>\<open>lhs\<close> (style_lhs_rhs fst) #>
   17.13 +  setup \<^binding>\<open>rhs\<close> (style_lhs_rhs snd) #>
   17.14 +  setup \<^binding>\<open>prem\<close> style_prem #>
   17.15 +  setup \<^binding>\<open>concl\<close> (Scan.succeed (K Logic.strip_imp_concl)) #>
   17.16 +  setup \<^binding>\<open>sub\<close> (Scan.succeed (K sub_term)));
   17.17  
   17.18  end;
    18.1 --- a/src/Pure/Thy/thy_output.ML	Wed Dec 06 15:46:35 2017 +0100
    18.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Dec 06 18:59:33 2017 +0100
    18.3 @@ -487,7 +487,7 @@
    18.4  
    18.5      (* present commands *)
    18.6  
    18.7 -    val document_tags = space_explode "," (Options.default_string @{system_option document_tags});
    18.8 +    val document_tags = space_explode "," (Options.default_string \<^system_option>\<open>document_tags\<close>);
    18.9  
   18.10      fun present_command tr span st st' =
   18.11        Toplevel.setmp_thread_position tr (present_span keywords document_tags span st st');
   18.12 @@ -511,23 +511,23 @@
   18.13  (* options *)
   18.14  
   18.15  val _ = Theory.setup
   18.16 - (add_option @{binding show_types} (Config.put show_types o boolean) #>
   18.17 -  add_option @{binding show_sorts} (Config.put show_sorts o boolean) #>
   18.18 -  add_option @{binding show_structs} (Config.put show_structs o boolean) #>
   18.19 -  add_option @{binding show_question_marks} (Config.put show_question_marks o boolean) #>
   18.20 -  add_option @{binding show_abbrevs} (Config.put show_abbrevs o boolean) #>
   18.21 -  add_option @{binding names_long} (Config.put Name_Space.names_long o boolean) #>
   18.22 -  add_option @{binding names_short} (Config.put Name_Space.names_short o boolean) #>
   18.23 -  add_option @{binding names_unique} (Config.put Name_Space.names_unique o boolean) #>
   18.24 -  add_option @{binding eta_contract} (Config.put Syntax_Trans.eta_contract o boolean) #>
   18.25 -  add_option @{binding display} (Config.put display o boolean) #>
   18.26 -  add_option @{binding break} (Config.put break o boolean) #>
   18.27 -  add_option @{binding quotes} (Config.put quotes o boolean) #>
   18.28 -  add_option @{binding mode} (add_wrapper o Print_Mode.with_modes o single) #>
   18.29 -  add_option @{binding margin} (Config.put margin o integer) #>
   18.30 -  add_option @{binding indent} (Config.put indent o integer) #>
   18.31 -  add_option @{binding source} (Config.put source o boolean) #>
   18.32 -  add_option @{binding goals_limit} (Config.put Goal_Display.goals_limit o integer));
   18.33 + (add_option \<^binding>\<open>show_types\<close> (Config.put show_types o boolean) #>
   18.34 +  add_option \<^binding>\<open>show_sorts\<close> (Config.put show_sorts o boolean) #>
   18.35 +  add_option \<^binding>\<open>show_structs\<close> (Config.put show_structs o boolean) #>
   18.36 +  add_option \<^binding>\<open>show_question_marks\<close> (Config.put show_question_marks o boolean) #>
   18.37 +  add_option \<^binding>\<open>show_abbrevs\<close> (Config.put show_abbrevs o boolean) #>
   18.38 +  add_option \<^binding>\<open>names_long\<close> (Config.put Name_Space.names_long o boolean) #>
   18.39 +  add_option \<^binding>\<open>names_short\<close> (Config.put Name_Space.names_short o boolean) #>
   18.40 +  add_option \<^binding>\<open>names_unique\<close> (Config.put Name_Space.names_unique o boolean) #>
   18.41 +  add_option \<^binding>\<open>eta_contract\<close> (Config.put Syntax_Trans.eta_contract o boolean) #>
   18.42 +  add_option \<^binding>\<open>display\<close> (Config.put display o boolean) #>
   18.43 +  add_option \<^binding>\<open>break\<close> (Config.put break o boolean) #>
   18.44 +  add_option \<^binding>\<open>quotes\<close> (Config.put quotes o boolean) #>
   18.45 +  add_option \<^binding>\<open>mode\<close> (add_wrapper o Print_Mode.with_modes o single) #>
   18.46 +  add_option \<^binding>\<open>margin\<close> (Config.put margin o integer) #>
   18.47 +  add_option \<^binding>\<open>indent\<close> (Config.put indent o integer) #>
   18.48 +  add_option \<^binding>\<open>source\<close> (Config.put source o boolean) #>
   18.49 +  add_option \<^binding>\<open>goals_limit\<close> (Config.put Goal_Display.goals_limit o integer));
   18.50  
   18.51  
   18.52  (* basic pretty printing *)
   18.53 @@ -647,20 +647,20 @@
   18.54  in
   18.55  
   18.56  val _ = Theory.setup
   18.57 - (basic_entities_style @{binding thm} (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
   18.58 -  basic_entity @{binding prop} (Term_Style.parse -- Args.prop) pretty_term_style #>
   18.59 -  basic_entity @{binding term} (Term_Style.parse -- Args.term) pretty_term_style #>
   18.60 -  basic_entity @{binding term_type} (Term_Style.parse -- Args.term) pretty_term_typ #>
   18.61 -  basic_entity @{binding typeof} (Term_Style.parse -- Args.term) pretty_term_typeof #>
   18.62 -  basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
   18.63 -  basic_entity @{binding abbrev} (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
   18.64 -  basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
   18.65 -  basic_entity @{binding locale} (Scan.lift (Parse.position Args.name)) pretty_locale #>
   18.66 -  basic_entity @{binding class} (Scan.lift Args.embedded_inner_syntax) pretty_class #>
   18.67 -  basic_entity @{binding type} (Scan.lift Args.embedded) pretty_type #>
   18.68 -  basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
   18.69 -  basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
   18.70 -  basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);
   18.71 + (basic_entities_style \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
   18.72 +  basic_entity \<^binding>\<open>prop\<close> (Term_Style.parse -- Args.prop) pretty_term_style #>
   18.73 +  basic_entity \<^binding>\<open>term\<close> (Term_Style.parse -- Args.term) pretty_term_style #>
   18.74 +  basic_entity \<^binding>\<open>term_type\<close> (Term_Style.parse -- Args.term) pretty_term_typ #>
   18.75 +  basic_entity \<^binding>\<open>typeof\<close> (Term_Style.parse -- Args.term) pretty_term_typeof #>
   18.76 +  basic_entity \<^binding>\<open>const\<close> (Args.const {proper = true, strict = false}) pretty_const #>
   18.77 +  basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
   18.78 +  basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #>
   18.79 +  basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.name)) pretty_locale #>
   18.80 +  basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #>
   18.81 +  basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded) pretty_type #>
   18.82 +  basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #>
   18.83 +  basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
   18.84 +  basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.name)) pretty_theory);
   18.85  
   18.86  end;
   18.87  
    19.1 --- a/src/Pure/Tools/bibtex.ML	Wed Dec 06 15:46:35 2017 +0100
    19.2 +++ b/src/Pure/Tools/bibtex.ML	Wed Dec 06 18:59:33 2017 +0100
    19.3 @@ -12,12 +12,12 @@
    19.4  structure Bibtex: BIBTEX =
    19.5  struct
    19.6  
    19.7 -val cite_macro = Attrib.setup_config_string @{binding cite_macro} (K "cite");
    19.8 +val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "cite");
    19.9  
   19.10  val _ =
   19.11    Theory.setup
   19.12 -   (Thy_Output.add_option @{binding cite_macro} (Config.put cite_macro) #>
   19.13 -    Thy_Output.antiquotation @{binding cite}
   19.14 +   (Thy_Output.add_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
   19.15 +    Thy_Output.antiquotation \<^binding>\<open>cite\<close>
   19.16        (Scan.lift
   19.17          (Scan.option (Parse.verbatim || Parse.cartouche) --
   19.18           Parse.and_list1 (Parse.position Args.name)))
    20.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Dec 06 15:46:35 2017 +0100
    20.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Dec 06 18:59:33 2017 +0100
    20.3 @@ -190,7 +190,7 @@
    20.4      val goal' = Thm.transfer thy' goal;
    20.5  
    20.6      fun limited_etac thm i =
    20.7 -      Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o
    20.8 +      Seq.take (Options.default_int \<^system_option>\<open>find_theorems_tactic_limit\<close>) o
    20.9          eresolve_tac ctxt' [thm] i;
   20.10      fun try_thm thm =
   20.11        if Thm.no_prems thm then resolve_tac ctxt' [thm] 1 goal'
   20.12 @@ -414,7 +414,7 @@
   20.13            else raw_matches;
   20.14  
   20.15          val len = length matches;
   20.16 -        val lim = the_default (Options.default_int @{system_option find_theorems_limit}) opt_limit;
   20.17 +        val lim = the_default (Options.default_int \<^system_option>\<open>find_theorems_limit\<close>) opt_limit;
   20.18        in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
   20.19  
   20.20      val find =
    21.1 --- a/src/Pure/Tools/jedit.ML	Wed Dec 06 15:46:35 2017 +0100
    21.2 +++ b/src/Pure/Tools/jedit.ML	Wed Dec 06 18:59:33 2017 +0100
    21.3 @@ -75,7 +75,7 @@
    21.4  
    21.5  val _ =
    21.6    Theory.setup
    21.7 -    (Thy_Output.antiquotation @{binding action} (Scan.lift (Parse.position Parse.embedded))
    21.8 +    (Thy_Output.antiquotation \<^binding>\<open>action\<close> (Scan.lift (Parse.position Parse.embedded))
    21.9        (fn {context = ctxt, ...} => fn (name, pos) =>
   21.10         (if Context_Position.is_reported ctxt pos then ignore (check_action (name, pos)) else ();
   21.11          Thy_Output.verbatim_text ctxt name)));
    22.1 --- a/src/Pure/Tools/named_theorems.ML	Wed Dec 06 15:46:35 2017 +0100
    22.2 +++ b/src/Pure/Tools/named_theorems.ML	Wed Dec 06 18:59:33 2017 +0100
    22.3 @@ -97,7 +97,7 @@
    22.4  (* ML antiquotation *)
    22.5  
    22.6  val _ = Theory.setup
    22.7 -  (ML_Antiquotation.inline @{binding named_theorems}
    22.8 +  (ML_Antiquotation.inline \<^binding>\<open>named_theorems\<close>
    22.9      (Args.context -- Scan.lift (Parse.position Args.embedded) >>
   22.10        (fn (ctxt, name) => ML_Syntax.print_string (check ctxt name))));
   22.11  
    23.1 --- a/src/Pure/Tools/plugin.ML	Wed Dec 06 15:46:35 2017 +0100
    23.2 +++ b/src/Pure/Tools/plugin.ML	Wed Dec 06 18:59:33 2017 +0100
    23.3 @@ -40,7 +40,7 @@
    23.4    #1 o Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt));
    23.5  
    23.6  val _ = Theory.setup
    23.7 -  (ML_Antiquotation.inline @{binding plugin}
    23.8 +  (ML_Antiquotation.inline \<^binding>\<open>plugin\<close>
    23.9      (Args.context -- Scan.lift (Parse.position Args.embedded)
   23.10        >> (ML_Syntax.print_string o uncurry check)));
   23.11  
    24.1 --- a/src/Pure/Tools/rail.ML	Wed Dec 06 15:46:35 2017 +0100
    24.2 +++ b/src/Pure/Tools/rail.ML	Wed Dec 06 18:59:33 2017 +0100
    24.3 @@ -374,7 +374,7 @@
    24.4    in Latex.environment "railoutput" (implode (map output_rule rules)) end;
    24.5  
    24.6  val _ = Theory.setup
    24.7 -  (Thy_Output.antiquotation @{binding rail} (Scan.lift Args.text_input)
    24.8 +  (Thy_Output.antiquotation \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
    24.9      (fn {state, context, ...} => output_rules state o read context));
   24.10  
   24.11  end;
    25.1 --- a/src/Pure/Tools/rule_insts.ML	Wed Dec 06 15:46:35 2017 +0100
    25.2 +++ b/src/Pure/Tools/rule_insts.ML	Wed Dec 06 18:59:33 2017 +0100
    25.3 @@ -182,7 +182,7 @@
    25.4      -- Parse.for_fixes;
    25.5  
    25.6  val _ = Theory.setup
    25.7 -  (Attrib.setup @{binding "where"}
    25.8 +  (Attrib.setup \<^binding>\<open>where\<close>
    25.9      (Scan.lift named_insts >> (fn args =>
   25.10        Thm.rule_attribute [] (fn context => uncurry (where_rule (Context.proof_of context)) args)))
   25.11      "named instantiation of theorem");
   25.12 @@ -202,7 +202,7 @@
   25.13  in
   25.14  
   25.15  val _ = Theory.setup
   25.16 -  (Attrib.setup @{binding "of"}
   25.17 +  (Attrib.setup \<^binding>\<open>of\<close>
   25.18      (Scan.lift (insts -- Parse.for_fixes) >> (fn args =>
   25.19        Thm.rule_attribute [] (fn context => uncurry (of_rule (Context.proof_of context)) args)))
   25.20      "positional instantiation of theorem");
   25.21 @@ -320,22 +320,22 @@
   25.22  (*warning: rule_tac etc. refer to dynamic subgoal context!*)
   25.23  
   25.24  val _ = Theory.setup
   25.25 - (Method.setup @{binding rule_tac} (method res_inst_tac resolve_tac)
   25.26 + (Method.setup \<^binding>\<open>rule_tac\<close> (method res_inst_tac resolve_tac)
   25.27      "apply rule (dynamic instantiation)" #>
   25.28 -  Method.setup @{binding erule_tac} (method eres_inst_tac eresolve_tac)
   25.29 +  Method.setup \<^binding>\<open>erule_tac\<close> (method eres_inst_tac eresolve_tac)
   25.30      "apply rule in elimination manner (dynamic instantiation)" #>
   25.31 -  Method.setup @{binding drule_tac} (method dres_inst_tac dresolve_tac)
   25.32 +  Method.setup \<^binding>\<open>drule_tac\<close> (method dres_inst_tac dresolve_tac)
   25.33      "apply rule in destruct manner (dynamic instantiation)" #>
   25.34 -  Method.setup @{binding frule_tac} (method forw_inst_tac forward_tac)
   25.35 +  Method.setup \<^binding>\<open>frule_tac\<close> (method forw_inst_tac forward_tac)
   25.36      "apply rule in forward manner (dynamic instantiation)" #>
   25.37 -  Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
   25.38 +  Method.setup \<^binding>\<open>cut_tac\<close> (method cut_inst_tac (K cut_rules_tac))
   25.39      "cut rule (dynamic instantiation)" #>
   25.40 -  Method.setup @{binding subgoal_tac}
   25.41 +  Method.setup \<^binding>\<open>subgoal_tac\<close>
   25.42      (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.embedded_inner_syntax -- Parse.for_fixes) >>
   25.43        (fn (quant, (props, fixes)) => fn ctxt =>
   25.44          SIMPLE_METHOD'' quant (EVERY' (map (fn prop => subgoal_tac ctxt prop fixes) props))))
   25.45      "insert subgoal (dynamic instantiation)" #>
   25.46 -  Method.setup @{binding thin_tac}
   25.47 +  Method.setup \<^binding>\<open>thin_tac\<close>
   25.48      (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
   25.49        (fn (quant, (prop, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop fixes)))
   25.50      "remove premise (dynamic instantiation)");
    26.1 --- a/src/Pure/Tools/simplifier_trace.ML	Wed Dec 06 15:46:35 2017 +0100
    26.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Wed Dec 06 18:59:33 2017 +0100
    26.3 @@ -438,10 +438,10 @@
    26.4      (fn (((interactive, mode), depth), memory) => config mode interactive depth memory)
    26.5  
    26.6  val _ = Theory.setup
    26.7 -  (Attrib.setup @{binding simp_break}
    26.8 +  (Attrib.setup \<^binding>\<open>simp_break\<close>
    26.9      (Scan.repeat Args.term_pattern >> breakpoint)
   26.10      "declaration of a simplifier breakpoint" #>
   26.11 -   Attrib.setup @{binding simp_trace_new} (Scan.lift config_parser)
   26.12 +   Attrib.setup \<^binding>\<open>simp_trace_new\<close> (Scan.lift config_parser)
   26.13      "simplifier trace configuration")
   26.14  
   26.15  end
    27.1 --- a/src/Pure/simplifier.ML	Wed Dec 06 15:46:35 2017 +0100
    27.2 +++ b/src/Pure/simplifier.ML	Wed Dec 06 18:59:33 2017 +0100
    27.3 @@ -112,7 +112,7 @@
    27.4  val the_simproc = Name_Space.get o get_simprocs;
    27.5  
    27.6  val _ = Theory.setup
    27.7 -  (ML_Antiquotation.value @{binding simproc}
    27.8 +  (ML_Antiquotation.value \<^binding>\<open>simproc\<close>
    27.9      (Args.context -- Scan.lift (Parse.position Args.embedded)
   27.10        >> (fn (ctxt, name) =>
   27.11          "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
   27.12 @@ -319,13 +319,13 @@
   27.13  (* setup attributes *)
   27.14  
   27.15  val _ = Theory.setup
   27.16 - (Attrib.setup @{binding simp} (Attrib.add_del simp_add simp_del)
   27.17 + (Attrib.setup \<^binding>\<open>simp\<close> (Attrib.add_del simp_add simp_del)
   27.18      "declaration of Simplifier rewrite rule" #>
   27.19 -  Attrib.setup @{binding cong} (Attrib.add_del cong_add cong_del)
   27.20 +  Attrib.setup \<^binding>\<open>cong\<close> (Attrib.add_del cong_add cong_del)
   27.21      "declaration of Simplifier congruence rule" #>
   27.22 -  Attrib.setup @{binding simproc} simproc_att
   27.23 +  Attrib.setup \<^binding>\<open>simproc\<close> simproc_att
   27.24      "declaration of simplification procedures" #>
   27.25 -  Attrib.setup @{binding simplified} simplified "simplified rule");
   27.26 +  Attrib.setup \<^binding>\<open>simplified\<close> simplified "simplified rule");
   27.27  
   27.28  
   27.29  
   27.30 @@ -368,12 +368,12 @@
   27.31  (** setup **)
   27.32  
   27.33  fun method_setup more_mods =
   27.34 -  Method.setup @{binding simp}
   27.35 +  Method.setup \<^binding>\<open>simp\<close>
   27.36      (simp_method more_mods (fn ctxt => fn tac => fn facts =>
   27.37        HEADGOAL (Method.insert_tac ctxt facts THEN'
   27.38          (CHANGED_PROP oo tac) ctxt)))
   27.39      "simplification" #>
   27.40 -  Method.setup @{binding simp_all}
   27.41 +  Method.setup \<^binding>\<open>simp_all\<close>
   27.42      (simp_method more_mods (fn ctxt => fn tac => fn facts =>
   27.43        ALLGOALS (Method.insert_tac ctxt facts) THEN
   27.44          (CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt))