# HG changeset patch
# User wenzelm
# Date 1395152998 -3600
# Node ID f70e69208a8c773923e9e4e6d8184de120e1b74d
# Parent  76c72f4d0667379aee496945fad8cc316ce2a2e9
more antiquotations;

diff -r 76c72f4d0667 -r f70e69208a8c src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Isar/class.ML	Tue Mar 18 15:29:58 2014 +0100
@@ -666,9 +666,9 @@
     default_intro_tac ctxt facts;
 
 val _ = Theory.setup
- (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac)))
+ (Method.setup @{binding intro_classes} (Scan.succeed (K (METHOD intro_classes_tac)))
     "back-chain introduction rules of classes" #>
-  Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
+  Method.setup @{binding default} (Attrib.thms >> (METHOD oo default_tac))
     "apply some intro/elim rule");
 
 end;
diff -r 76c72f4d0667 -r f70e69208a8c src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Isar/code.ML	Tue Mar 18 15:29:58 2014 +0100
@@ -1285,7 +1285,7 @@
       || Scan.succeed (mk_attribute add_eqn_maybe_abs);
   in
     Datatype_Interpretation.init
-    #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
+    #> Attrib.setup @{binding code} (Scan.lift code_attribute_parser)
         "declare theorems for code generation"
   end);
 
diff -r 76c72f4d0667 -r f70e69208a8c src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Isar/context_rules.ML	Tue Mar 18 15:29:58 2014 +0100
@@ -209,13 +209,13 @@
     Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
 
 val _ = Theory.setup
- (Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
+ (Attrib.setup @{binding intro} (add intro_bang intro intro_query)
     "declaration of introduction rule" #>
-  Attrib.setup (Binding.name "elim") (add elim_bang elim elim_query)
+  Attrib.setup @{binding elim} (add elim_bang elim elim_query)
     "declaration of elimination rule" #>
-  Attrib.setup (Binding.name "dest") (add dest_bang dest dest_query)
+  Attrib.setup @{binding dest} (add dest_bang dest dest_query)
     "declaration of destruction rule" #>
-  Attrib.setup (Binding.name "rule") (Scan.lift Args.del >> K rule_del)
+  Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
     "remove declaration of intro/elim/dest rule");
 
 end;
diff -r 76c72f4d0667 -r f70e69208a8c src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 18 15:29:58 2014 +0100
@@ -247,9 +247,9 @@
     handle Toplevel.UNDEF => error "No goal present";
 
 val _ = Theory.setup
-  (ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "state"))
+  (ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state})
     (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
-   ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "goal"))
+   ML_Antiquotation.value (Binding.qualify true "Isar" @{binding goal})
     (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
 
 
diff -r 76c72f4d0667 -r f70e69208a8c src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Mar 18 15:29:58 2014 +0100
@@ -622,9 +622,9 @@
 val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
 
 val _ = Theory.setup
- (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
+ (Method.setup @{binding intro_locales} (Scan.succeed (METHOD o try_intro_locales_tac false))
     "back-chain introduction rules of locales without unfolding predicates" #>
-  Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
+  Method.setup @{binding unfold_locales} (Scan.succeed (METHOD o try_intro_locales_tac true))
     "back-chain all introduction rules of locales");
 
 
diff -r 76c72f4d0667 -r f70e69208a8c src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Isar/method.ML	Tue Mar 18 15:29:58 2014 +0100
@@ -201,7 +201,7 @@
 
 (* rule etc. -- single-step refinements *)
 
-val rule_trace = Attrib.setup_config_bool (Binding.name "rule_trace") (fn _ => false);
+val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false);
 
 fun trace ctxt rules =
   if Config.get ctxt rule_trace andalso not (null rules) then
@@ -478,38 +478,38 @@
 (* theory setup *)
 
 val _ = Theory.setup
- (setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
-  setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
-  setup (Binding.name "-") (Scan.succeed (K insert_facts))
+ (setup @{binding fail} (Scan.succeed (K fail)) "force failure" #>
+  setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #>
+  setup @{binding "-"} (Scan.succeed (K insert_facts))
     "do nothing (insert current facts only)" #>
-  setup (Binding.name "insert") (Attrib.thms >> (K o insert))
+  setup @{binding insert} (Attrib.thms >> (K o insert))
     "insert theorems, ignoring facts (improper)" #>
-  setup (Binding.name "intro") (Attrib.thms >> (K o intro))
+  setup @{binding intro} (Attrib.thms >> (K o intro))
     "repeatedly apply introduction rules" #>
-  setup (Binding.name "elim") (Attrib.thms >> (K o elim))
+  setup @{binding elim} (Attrib.thms >> (K o elim))
     "repeatedly apply elimination rules" #>
-  setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #>
-  setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #>
-  setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> atomize)
+  setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #>
+  setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #>
+  setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize)
     "present local premises as object-level statements" #>
-  setup (Binding.name "rule") (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
+  setup @{binding rule} (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
     "apply some intro/elim rule" #>
-  setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #>
-  setup (Binding.name "drule") (xrule_meth drule) "apply rule in destruct manner (improper)" #>
-  setup (Binding.name "frule") (xrule_meth frule) "apply rule in forward manner (improper)" #>
-  setup (Binding.name "this") (Scan.succeed (K this)) "apply current facts as rules" #>
-  setup (Binding.name "fact") (Attrib.thms >> fact) "composition by facts from context" #>
-  setup (Binding.name "assumption") (Scan.succeed assumption)
+  setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #>
+  setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #>
+  setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #>
+  setup @{binding this} (Scan.succeed (K this)) "apply current facts as rules" #>
+  setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #>
+  setup @{binding assumption} (Scan.succeed assumption)
     "proof by assumption, preferring facts" #>
-  setup (Binding.name "rename_tac") (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
+  setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
     (fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs))))
     "rename parameters of goal" #>
-  setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
+  setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
     (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
       "rotate assumptions of goal" #>
-  setup (Binding.name "tactic") (Scan.lift Args.name_source_position >> tactic)
+  setup @{binding tactic} (Scan.lift Args.name_source_position >> tactic)
     "ML tactic as proof method" #>
-  setup (Binding.name "raw_tactic") (Scan.lift Args.name_source_position >> raw_tactic)
+  setup @{binding raw_tactic} (Scan.lift Args.name_source_position >> raw_tactic)
     "ML tactic as raw proof method");
 
 
diff -r 76c72f4d0667 -r f70e69208a8c src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Thy/term_style.ML	Tue Mar 18 15:29:58 2014 +0100
@@ -84,10 +84,10 @@
   | sub_term t = t;
 
 val _ = Theory.setup
- (setup (Binding.name "lhs") (style_lhs_rhs fst) #>
-  setup (Binding.name "rhs") (style_lhs_rhs snd) #>
-  setup (Binding.name "prem") style_prem #>
-  setup (Binding.name "concl") (Scan.succeed (K Logic.strip_imp_concl)) #>
-  setup (Binding.name "sub") (Scan.succeed (K sub_term)));
+ (setup @{binding lhs} (style_lhs_rhs fst) #>
+  setup @{binding rhs} (style_lhs_rhs snd) #>
+  setup @{binding prem} style_prem #>
+  setup @{binding concl} (Scan.succeed (K Logic.strip_imp_concl)) #>
+  setup @{binding sub} (Scan.succeed (K sub_term)));
 
 end;
diff -r 76c72f4d0667 -r f70e69208a8c src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Thy/thy_load.ML	Tue Mar 18 15:29:58 2014 +0100
@@ -229,11 +229,11 @@
 in
 
 val _ = Theory.setup
- (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
+ (Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
     (file_antiq true o #context) #>
-  Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
+  Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
     (file_antiq false o #context) #>
-  ML_Antiquotation.value (Binding.name "path")
+  ML_Antiquotation.value @{binding path}
     (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
       let val path = check_path true ctxt Path.current arg
       in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
diff -r 76c72f4d0667 -r f70e69208a8c src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Mar 18 15:29:58 2014 +0100
@@ -437,23 +437,23 @@
 (* options *)
 
 val _ = Theory.setup
- (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
-  add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
-  add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
-  add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
-  add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
-  add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
-  add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
-  add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
-  add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
-  add_option (Binding.name "display") (Config.put display o boolean) #>
-  add_option (Binding.name "break") (Config.put break o boolean) #>
-  add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
-  add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
-  add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
-  add_option (Binding.name "indent") (Config.put indent o integer) #>
-  add_option (Binding.name "source") (Config.put source o boolean) #>
-  add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer));
+ (add_option @{binding show_types} (Config.put show_types o boolean) #>
+  add_option @{binding show_sorts} (Config.put show_sorts o boolean) #>
+  add_option @{binding show_structs} (Config.put show_structs o boolean) #>
+  add_option @{binding show_question_marks} (Config.put show_question_marks o boolean) #>
+  add_option @{binding show_abbrevs} (Config.put show_abbrevs o boolean) #>
+  add_option @{binding names_long} (Config.put Name_Space.names_long o boolean) #>
+  add_option @{binding names_short} (Config.put Name_Space.names_short o boolean) #>
+  add_option @{binding names_unique} (Config.put Name_Space.names_unique o boolean) #>
+  add_option @{binding eta_contract} (Config.put Syntax_Trans.eta_contract o boolean) #>
+  add_option @{binding display} (Config.put display o boolean) #>
+  add_option @{binding break} (Config.put break o boolean) #>
+  add_option @{binding quotes} (Config.put quotes o boolean) #>
+  add_option @{binding mode} (add_wrapper o Print_Mode.with_modes o single) #>
+  add_option @{binding margin} (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
+  add_option @{binding indent} (Config.put indent o integer) #>
+  add_option @{binding source} (Config.put source o boolean) #>
+  add_option @{binding goals_limit} (Config.put Goal_Display.goals_limit o integer));
 
 
 (* basic pretty printing *)
@@ -565,20 +565,20 @@
 in
 
 val _ = Theory.setup
- (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
-  basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
-  basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
-  basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
-  basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
-  basic_entity (Binding.name "const") (Args.const {proper = true, strict = false}) pretty_const #>
-  basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
-  basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
-  basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
-  basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
-  basic_entity (Binding.name "text") (Scan.lift Args.name_source_position) pretty_text_report #>
-  basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
-  basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
-  basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory);
+ (basic_entities_style @{binding thm} (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
+  basic_entity @{binding prop} (Term_Style.parse -- Args.prop) pretty_term_style #>
+  basic_entity @{binding term} (Term_Style.parse -- Args.term) pretty_term_style #>
+  basic_entity @{binding term_type} (Term_Style.parse -- Args.term) pretty_term_typ #>
+  basic_entity @{binding typeof} (Term_Style.parse -- Args.term) pretty_term_typeof #>
+  basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
+  basic_entity @{binding abbrev} (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
+  basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
+  basic_entity @{binding class} (Scan.lift Args.name_inner_syntax) pretty_class #>
+  basic_entity @{binding type} (Scan.lift Args.name) pretty_type #>
+  basic_entity @{binding text} (Scan.lift Args.name_source_position) pretty_text_report #>
+  basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
+  basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
+  basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);
 
 end;
 
@@ -600,8 +600,8 @@
 in
 
 val _ = Theory.setup
- (goal_state (Binding.name "goals") true #>
-  goal_state (Binding.name "subgoals") false);
+ (goal_state @{binding goals} true #>
+  goal_state @{binding subgoals} false);
 
 end;
 
@@ -611,7 +611,7 @@
 val _ = Keyword.define ("by", NONE);  (*overlap with command category*)
 
 val _ = Theory.setup
-  (antiquotation (Binding.name "lemma")
+  (antiquotation @{binding lemma}
     (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
       Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse))
     (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
@@ -654,18 +654,18 @@
 in
 
 val _ = Theory.setup
- (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
-  ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
-  ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
-  ml_text (Binding.name "ML_structure")
+ (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>
+  ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #>
+  ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #>
+  ml_text @{binding ML_structure}
     (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
 
-  ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
+  ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
     (fn source =>
       ML_Lex.read Position.none ("ML_Env.check_functor " ^
         ML_Syntax.print_string (#1 (Symbol_Pos.source_content source)))) #>
 
-  ml_text (Binding.name "ML_text") (K []));
+  ml_text @{binding ML_text} (K []));
 
 end;
 
@@ -673,7 +673,7 @@
 (* URLs *)
 
 val _ = Theory.setup
-  (antiquotation (Binding.name "url") (Scan.lift (Parse.position Parse.name))
+  (antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
     (fn {context = ctxt, ...} => fn (name, pos) =>
       (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
        enclose "\\url{" "}" name)));
diff -r 76c72f4d0667 -r f70e69208a8c src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/pure_syn.ML	Tue Mar 18 15:29:58 2014 +0100
@@ -9,8 +9,7 @@
 
 val _ =
   Outer_Syntax.command
-    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.file "pure_syn.ML")
-    "begin theory context"
+    (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
     (Thy_Header.args >> (fn header =>
       Toplevel.print o
         Toplevel.init_theory
@@ -18,8 +17,7 @@
 
 val _ =
   Outer_Syntax.command
-    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.file "pure_syn.ML")
-    "ML text from file"
+    (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file"
     (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
         let
           val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
diff -r 76c72f4d0667 -r f70e69208a8c src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/simplifier.ML	Tue Mar 18 15:29:58 2014 +0100
@@ -144,7 +144,7 @@
 val the_simproc = Name_Space.get o get_simprocs;
 
 val _ = Theory.setup
-  (ML_Antiquotation.value (Binding.name "simproc")
+  (ML_Antiquotation.value @{binding simproc}
     (Args.context -- Scan.lift (Parse.position Args.name)
       >> (fn (ctxt, name) =>
         "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
@@ -315,13 +315,13 @@
 (* setup attributes *)
 
 val _ = Theory.setup
- (Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
+ (Attrib.setup @{binding simp} (Attrib.add_del simp_add simp_del)
     "declaration of Simplifier rewrite rule" #>
-  Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
+  Attrib.setup @{binding cong} (Attrib.add_del cong_add cong_del)
     "declaration of Simplifier congruence rule" #>
-  Attrib.setup (Binding.name "simproc") simproc_att
+  Attrib.setup @{binding simproc} simproc_att
     "declaration of simplification procedures" #>
-  Attrib.setup (Binding.name "simplified") simplified "simplified rule");
+  Attrib.setup @{binding simplified} simplified "simplified rule");
 
 
 
@@ -362,12 +362,12 @@
 (** setup **)
 
 fun method_setup more_mods =
-  Method.setup (Binding.name simpN)
+  Method.setup @{binding simp}
     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
       HEADGOAL (Method.insert_tac facts THEN'
         (CHANGED_PROP oo tac) ctxt)))
     "simplification" #>
-  Method.setup (Binding.name "simp_all")
+  Method.setup @{binding simp_all}
     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
       ALLGOALS (Method.insert_tac facts) THEN
         (CHANGED_PROP o PARALLEL_GOALS o ALLGOALS o tac) ctxt))