more antiquotations;
authorwenzelm
Tue Mar 18 15:29:58 2014 +0100 (2014-03-18 ago)
changeset 56204f70e69208a8c
parent 56203 76c72f4d0667
child 56205 ceb8a93460b7
more antiquotations;
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/Thy/term_style.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_output.ML
src/Pure/pure_syn.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/Isar/class.ML	Tue Mar 18 13:36:28 2014 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Mar 18 15:29:58 2014 +0100
     1.3 @@ -666,9 +666,9 @@
     1.4      default_intro_tac ctxt facts;
     1.5  
     1.6  val _ = Theory.setup
     1.7 - (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac)))
     1.8 + (Method.setup @{binding intro_classes} (Scan.succeed (K (METHOD intro_classes_tac)))
     1.9      "back-chain introduction rules of classes" #>
    1.10 -  Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
    1.11 +  Method.setup @{binding default} (Attrib.thms >> (METHOD oo default_tac))
    1.12      "apply some intro/elim rule");
    1.13  
    1.14  end;
     2.1 --- a/src/Pure/Isar/code.ML	Tue Mar 18 13:36:28 2014 +0100
     2.2 +++ b/src/Pure/Isar/code.ML	Tue Mar 18 15:29:58 2014 +0100
     2.3 @@ -1285,7 +1285,7 @@
     2.4        || Scan.succeed (mk_attribute add_eqn_maybe_abs);
     2.5    in
     2.6      Datatype_Interpretation.init
     2.7 -    #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
     2.8 +    #> Attrib.setup @{binding code} (Scan.lift code_attribute_parser)
     2.9          "declare theorems for code generation"
    2.10    end);
    2.11  
     3.1 --- a/src/Pure/Isar/context_rules.ML	Tue Mar 18 13:36:28 2014 +0100
     3.2 +++ b/src/Pure/Isar/context_rules.ML	Tue Mar 18 15:29:58 2014 +0100
     3.3 @@ -209,13 +209,13 @@
     3.4      Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
     3.5  
     3.6  val _ = Theory.setup
     3.7 - (Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
     3.8 + (Attrib.setup @{binding intro} (add intro_bang intro intro_query)
     3.9      "declaration of introduction rule" #>
    3.10 -  Attrib.setup (Binding.name "elim") (add elim_bang elim elim_query)
    3.11 +  Attrib.setup @{binding elim} (add elim_bang elim elim_query)
    3.12      "declaration of elimination rule" #>
    3.13 -  Attrib.setup (Binding.name "dest") (add dest_bang dest dest_query)
    3.14 +  Attrib.setup @{binding dest} (add dest_bang dest dest_query)
    3.15      "declaration of destruction rule" #>
    3.16 -  Attrib.setup (Binding.name "rule") (Scan.lift Args.del >> K rule_del)
    3.17 +  Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
    3.18      "remove declaration of intro/elim/dest rule");
    3.19  
    3.20  end;
     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 18 13:36:28 2014 +0100
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 18 15:29:58 2014 +0100
     4.3 @@ -247,9 +247,9 @@
     4.4      handle Toplevel.UNDEF => error "No goal present";
     4.5  
     4.6  val _ = Theory.setup
     4.7 -  (ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "state"))
     4.8 +  (ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state})
     4.9      (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
    4.10 -   ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "goal"))
    4.11 +   ML_Antiquotation.value (Binding.qualify true "Isar" @{binding goal})
    4.12      (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
    4.13  
    4.14  
     5.1 --- a/src/Pure/Isar/locale.ML	Tue Mar 18 13:36:28 2014 +0100
     5.2 +++ b/src/Pure/Isar/locale.ML	Tue Mar 18 15:29:58 2014 +0100
     5.3 @@ -622,9 +622,9 @@
     5.4  val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
     5.5  
     5.6  val _ = Theory.setup
     5.7 - (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
     5.8 + (Method.setup @{binding intro_locales} (Scan.succeed (METHOD o try_intro_locales_tac false))
     5.9      "back-chain introduction rules of locales without unfolding predicates" #>
    5.10 -  Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
    5.11 +  Method.setup @{binding unfold_locales} (Scan.succeed (METHOD o try_intro_locales_tac true))
    5.12      "back-chain all introduction rules of locales");
    5.13  
    5.14  
     6.1 --- a/src/Pure/Isar/method.ML	Tue Mar 18 13:36:28 2014 +0100
     6.2 +++ b/src/Pure/Isar/method.ML	Tue Mar 18 15:29:58 2014 +0100
     6.3 @@ -201,7 +201,7 @@
     6.4  
     6.5  (* rule etc. -- single-step refinements *)
     6.6  
     6.7 -val rule_trace = Attrib.setup_config_bool (Binding.name "rule_trace") (fn _ => false);
     6.8 +val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false);
     6.9  
    6.10  fun trace ctxt rules =
    6.11    if Config.get ctxt rule_trace andalso not (null rules) then
    6.12 @@ -478,38 +478,38 @@
    6.13  (* theory setup *)
    6.14  
    6.15  val _ = Theory.setup
    6.16 - (setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
    6.17 -  setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
    6.18 -  setup (Binding.name "-") (Scan.succeed (K insert_facts))
    6.19 + (setup @{binding fail} (Scan.succeed (K fail)) "force failure" #>
    6.20 +  setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #>
    6.21 +  setup @{binding "-"} (Scan.succeed (K insert_facts))
    6.22      "do nothing (insert current facts only)" #>
    6.23 -  setup (Binding.name "insert") (Attrib.thms >> (K o insert))
    6.24 +  setup @{binding insert} (Attrib.thms >> (K o insert))
    6.25      "insert theorems, ignoring facts (improper)" #>
    6.26 -  setup (Binding.name "intro") (Attrib.thms >> (K o intro))
    6.27 +  setup @{binding intro} (Attrib.thms >> (K o intro))
    6.28      "repeatedly apply introduction rules" #>
    6.29 -  setup (Binding.name "elim") (Attrib.thms >> (K o elim))
    6.30 +  setup @{binding elim} (Attrib.thms >> (K o elim))
    6.31      "repeatedly apply elimination rules" #>
    6.32 -  setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #>
    6.33 -  setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #>
    6.34 -  setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> atomize)
    6.35 +  setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #>
    6.36 +  setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #>
    6.37 +  setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize)
    6.38      "present local premises as object-level statements" #>
    6.39 -  setup (Binding.name "rule") (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
    6.40 +  setup @{binding rule} (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
    6.41      "apply some intro/elim rule" #>
    6.42 -  setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #>
    6.43 -  setup (Binding.name "drule") (xrule_meth drule) "apply rule in destruct manner (improper)" #>
    6.44 -  setup (Binding.name "frule") (xrule_meth frule) "apply rule in forward manner (improper)" #>
    6.45 -  setup (Binding.name "this") (Scan.succeed (K this)) "apply current facts as rules" #>
    6.46 -  setup (Binding.name "fact") (Attrib.thms >> fact) "composition by facts from context" #>
    6.47 -  setup (Binding.name "assumption") (Scan.succeed assumption)
    6.48 +  setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #>
    6.49 +  setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #>
    6.50 +  setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #>
    6.51 +  setup @{binding this} (Scan.succeed (K this)) "apply current facts as rules" #>
    6.52 +  setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #>
    6.53 +  setup @{binding assumption} (Scan.succeed assumption)
    6.54      "proof by assumption, preferring facts" #>
    6.55 -  setup (Binding.name "rename_tac") (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
    6.56 +  setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
    6.57      (fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs))))
    6.58      "rename parameters of goal" #>
    6.59 -  setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
    6.60 +  setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
    6.61      (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
    6.62        "rotate assumptions of goal" #>
    6.63 -  setup (Binding.name "tactic") (Scan.lift Args.name_source_position >> tactic)
    6.64 +  setup @{binding tactic} (Scan.lift Args.name_source_position >> tactic)
    6.65      "ML tactic as proof method" #>
    6.66 -  setup (Binding.name "raw_tactic") (Scan.lift Args.name_source_position >> raw_tactic)
    6.67 +  setup @{binding raw_tactic} (Scan.lift Args.name_source_position >> raw_tactic)
    6.68      "ML tactic as raw proof method");
    6.69  
    6.70  
     7.1 --- a/src/Pure/Thy/term_style.ML	Tue Mar 18 13:36:28 2014 +0100
     7.2 +++ b/src/Pure/Thy/term_style.ML	Tue Mar 18 15:29:58 2014 +0100
     7.3 @@ -84,10 +84,10 @@
     7.4    | sub_term t = t;
     7.5  
     7.6  val _ = Theory.setup
     7.7 - (setup (Binding.name "lhs") (style_lhs_rhs fst) #>
     7.8 -  setup (Binding.name "rhs") (style_lhs_rhs snd) #>
     7.9 -  setup (Binding.name "prem") style_prem #>
    7.10 -  setup (Binding.name "concl") (Scan.succeed (K Logic.strip_imp_concl)) #>
    7.11 -  setup (Binding.name "sub") (Scan.succeed (K sub_term)));
    7.12 + (setup @{binding lhs} (style_lhs_rhs fst) #>
    7.13 +  setup @{binding rhs} (style_lhs_rhs snd) #>
    7.14 +  setup @{binding prem} style_prem #>
    7.15 +  setup @{binding concl} (Scan.succeed (K Logic.strip_imp_concl)) #>
    7.16 +  setup @{binding sub} (Scan.succeed (K sub_term)));
    7.17  
    7.18  end;
     8.1 --- a/src/Pure/Thy/thy_load.ML	Tue Mar 18 13:36:28 2014 +0100
     8.2 +++ b/src/Pure/Thy/thy_load.ML	Tue Mar 18 15:29:58 2014 +0100
     8.3 @@ -229,11 +229,11 @@
     8.4  in
     8.5  
     8.6  val _ = Theory.setup
     8.7 - (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
     8.8 + (Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
     8.9      (file_antiq true o #context) #>
    8.10 -  Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
    8.11 +  Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
    8.12      (file_antiq false o #context) #>
    8.13 -  ML_Antiquotation.value (Binding.name "path")
    8.14 +  ML_Antiquotation.value @{binding path}
    8.15      (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
    8.16        let val path = check_path true ctxt Path.current arg
    8.17        in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
     9.1 --- a/src/Pure/Thy/thy_output.ML	Tue Mar 18 13:36:28 2014 +0100
     9.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Mar 18 15:29:58 2014 +0100
     9.3 @@ -437,23 +437,23 @@
     9.4  (* options *)
     9.5  
     9.6  val _ = Theory.setup
     9.7 - (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
     9.8 -  add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
     9.9 -  add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
    9.10 -  add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
    9.11 -  add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
    9.12 -  add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
    9.13 -  add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
    9.14 -  add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
    9.15 -  add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
    9.16 -  add_option (Binding.name "display") (Config.put display o boolean) #>
    9.17 -  add_option (Binding.name "break") (Config.put break o boolean) #>
    9.18 -  add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
    9.19 -  add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
    9.20 -  add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
    9.21 -  add_option (Binding.name "indent") (Config.put indent o integer) #>
    9.22 -  add_option (Binding.name "source") (Config.put source o boolean) #>
    9.23 -  add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer));
    9.24 + (add_option @{binding show_types} (Config.put show_types o boolean) #>
    9.25 +  add_option @{binding show_sorts} (Config.put show_sorts o boolean) #>
    9.26 +  add_option @{binding show_structs} (Config.put show_structs o boolean) #>
    9.27 +  add_option @{binding show_question_marks} (Config.put show_question_marks o boolean) #>
    9.28 +  add_option @{binding show_abbrevs} (Config.put show_abbrevs o boolean) #>
    9.29 +  add_option @{binding names_long} (Config.put Name_Space.names_long o boolean) #>
    9.30 +  add_option @{binding names_short} (Config.put Name_Space.names_short o boolean) #>
    9.31 +  add_option @{binding names_unique} (Config.put Name_Space.names_unique o boolean) #>
    9.32 +  add_option @{binding eta_contract} (Config.put Syntax_Trans.eta_contract o boolean) #>
    9.33 +  add_option @{binding display} (Config.put display o boolean) #>
    9.34 +  add_option @{binding break} (Config.put break o boolean) #>
    9.35 +  add_option @{binding quotes} (Config.put quotes o boolean) #>
    9.36 +  add_option @{binding mode} (add_wrapper o Print_Mode.with_modes o single) #>
    9.37 +  add_option @{binding margin} (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
    9.38 +  add_option @{binding indent} (Config.put indent o integer) #>
    9.39 +  add_option @{binding source} (Config.put source o boolean) #>
    9.40 +  add_option @{binding goals_limit} (Config.put Goal_Display.goals_limit o integer));
    9.41  
    9.42  
    9.43  (* basic pretty printing *)
    9.44 @@ -565,20 +565,20 @@
    9.45  in
    9.46  
    9.47  val _ = Theory.setup
    9.48 - (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
    9.49 -  basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
    9.50 -  basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
    9.51 -  basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
    9.52 -  basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
    9.53 -  basic_entity (Binding.name "const") (Args.const {proper = true, strict = false}) pretty_const #>
    9.54 -  basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
    9.55 -  basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
    9.56 -  basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
    9.57 -  basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
    9.58 -  basic_entity (Binding.name "text") (Scan.lift Args.name_source_position) pretty_text_report #>
    9.59 -  basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
    9.60 -  basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
    9.61 -  basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory);
    9.62 + (basic_entities_style @{binding thm} (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
    9.63 +  basic_entity @{binding prop} (Term_Style.parse -- Args.prop) pretty_term_style #>
    9.64 +  basic_entity @{binding term} (Term_Style.parse -- Args.term) pretty_term_style #>
    9.65 +  basic_entity @{binding term_type} (Term_Style.parse -- Args.term) pretty_term_typ #>
    9.66 +  basic_entity @{binding typeof} (Term_Style.parse -- Args.term) pretty_term_typeof #>
    9.67 +  basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
    9.68 +  basic_entity @{binding abbrev} (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
    9.69 +  basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
    9.70 +  basic_entity @{binding class} (Scan.lift Args.name_inner_syntax) pretty_class #>
    9.71 +  basic_entity @{binding type} (Scan.lift Args.name) pretty_type #>
    9.72 +  basic_entity @{binding text} (Scan.lift Args.name_source_position) pretty_text_report #>
    9.73 +  basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
    9.74 +  basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
    9.75 +  basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);
    9.76  
    9.77  end;
    9.78  
    9.79 @@ -600,8 +600,8 @@
    9.80  in
    9.81  
    9.82  val _ = Theory.setup
    9.83 - (goal_state (Binding.name "goals") true #>
    9.84 -  goal_state (Binding.name "subgoals") false);
    9.85 + (goal_state @{binding goals} true #>
    9.86 +  goal_state @{binding subgoals} false);
    9.87  
    9.88  end;
    9.89  
    9.90 @@ -611,7 +611,7 @@
    9.91  val _ = Keyword.define ("by", NONE);  (*overlap with command category*)
    9.92  
    9.93  val _ = Theory.setup
    9.94 -  (antiquotation (Binding.name "lemma")
    9.95 +  (antiquotation @{binding lemma}
    9.96      (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
    9.97        Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse))
    9.98      (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
    9.99 @@ -654,18 +654,18 @@
   9.100  in
   9.101  
   9.102  val _ = Theory.setup
   9.103 - (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
   9.104 -  ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
   9.105 -  ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
   9.106 -  ml_text (Binding.name "ML_structure")
   9.107 + (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>
   9.108 +  ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #>
   9.109 +  ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #>
   9.110 +  ml_text @{binding ML_structure}
   9.111      (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
   9.112  
   9.113 -  ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
   9.114 +  ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
   9.115      (fn source =>
   9.116        ML_Lex.read Position.none ("ML_Env.check_functor " ^
   9.117          ML_Syntax.print_string (#1 (Symbol_Pos.source_content source)))) #>
   9.118  
   9.119 -  ml_text (Binding.name "ML_text") (K []));
   9.120 +  ml_text @{binding ML_text} (K []));
   9.121  
   9.122  end;
   9.123  
   9.124 @@ -673,7 +673,7 @@
   9.125  (* URLs *)
   9.126  
   9.127  val _ = Theory.setup
   9.128 -  (antiquotation (Binding.name "url") (Scan.lift (Parse.position Parse.name))
   9.129 +  (antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
   9.130      (fn {context = ctxt, ...} => fn (name, pos) =>
   9.131        (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
   9.132         enclose "\\url{" "}" name)));
    10.1 --- a/src/Pure/pure_syn.ML	Tue Mar 18 13:36:28 2014 +0100
    10.2 +++ b/src/Pure/pure_syn.ML	Tue Mar 18 15:29:58 2014 +0100
    10.3 @@ -9,8 +9,7 @@
    10.4  
    10.5  val _ =
    10.6    Outer_Syntax.command
    10.7 -    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.file "pure_syn.ML")
    10.8 -    "begin theory context"
    10.9 +    (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
   10.10      (Thy_Header.args >> (fn header =>
   10.11        Toplevel.print o
   10.12          Toplevel.init_theory
   10.13 @@ -18,8 +17,7 @@
   10.14  
   10.15  val _ =
   10.16    Outer_Syntax.command
   10.17 -    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.file "pure_syn.ML")
   10.18 -    "ML text from file"
   10.19 +    (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file"
   10.20      (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
   10.21          let
   10.22            val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
    11.1 --- a/src/Pure/simplifier.ML	Tue Mar 18 13:36:28 2014 +0100
    11.2 +++ b/src/Pure/simplifier.ML	Tue Mar 18 15:29:58 2014 +0100
    11.3 @@ -144,7 +144,7 @@
    11.4  val the_simproc = Name_Space.get o get_simprocs;
    11.5  
    11.6  val _ = Theory.setup
    11.7 -  (ML_Antiquotation.value (Binding.name "simproc")
    11.8 +  (ML_Antiquotation.value @{binding simproc}
    11.9      (Args.context -- Scan.lift (Parse.position Args.name)
   11.10        >> (fn (ctxt, name) =>
   11.11          "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
   11.12 @@ -315,13 +315,13 @@
   11.13  (* setup attributes *)
   11.14  
   11.15  val _ = Theory.setup
   11.16 - (Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
   11.17 + (Attrib.setup @{binding simp} (Attrib.add_del simp_add simp_del)
   11.18      "declaration of Simplifier rewrite rule" #>
   11.19 -  Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
   11.20 +  Attrib.setup @{binding cong} (Attrib.add_del cong_add cong_del)
   11.21      "declaration of Simplifier congruence rule" #>
   11.22 -  Attrib.setup (Binding.name "simproc") simproc_att
   11.23 +  Attrib.setup @{binding simproc} simproc_att
   11.24      "declaration of simplification procedures" #>
   11.25 -  Attrib.setup (Binding.name "simplified") simplified "simplified rule");
   11.26 +  Attrib.setup @{binding simplified} simplified "simplified rule");
   11.27  
   11.28  
   11.29  
   11.30 @@ -362,12 +362,12 @@
   11.31  (** setup **)
   11.32  
   11.33  fun method_setup more_mods =
   11.34 -  Method.setup (Binding.name simpN)
   11.35 +  Method.setup @{binding simp}
   11.36      (simp_method more_mods (fn ctxt => fn tac => fn facts =>
   11.37        HEADGOAL (Method.insert_tac facts THEN'
   11.38          (CHANGED_PROP oo tac) ctxt)))
   11.39      "simplification" #>
   11.40 -  Method.setup (Binding.name "simp_all")
   11.41 +  Method.setup @{binding simp_all}
   11.42      (simp_method more_mods (fn ctxt => fn tac => fn facts =>
   11.43        ALLGOALS (Method.insert_tac facts) THEN
   11.44          (CHANGED_PROP o PARALLEL_GOALS o ALLGOALS o tac) ctxt))