standardized aliases;
authorwenzelm
Sat, 27 Jul 2013 16:35:51 +0200
changeset 52732 b4da1f2ec73f
parent 52731 dacd47a0633f
child 52733 98f94010d78d
standardized aliases;
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/SMT_Examples/boogie.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/z3_proof_methods.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/inductive.ML
src/Provers/classical.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/rule_insts.ML
src/Pure/goal.ML
src/Tools/case_product.ML
src/Tools/eqsubst.ML
src/Tools/induct.ML
src/Tools/intuitionistic.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -73,7 +73,7 @@
     val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible]
     val (full_tname, Ts) = dest_Type newT
     val lhs_sorts = map (snd o dest_TFree) Ts
-    val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1
+    val tac = rtac (@{thm typedef_cpo} OF cpo_thms) 1
     val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy
     (* transfer thms so that they will know about the new cpo instance *)
     val cpo_thms' = map (Thm.transfer thy) cpo_thms
@@ -112,7 +112,7 @@
     val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem]
     val (full_tname, Ts) = dest_Type newT
     val lhs_sorts = map (snd o dest_TFree) Ts
-    val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
+    val tac = rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
     val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy
     val pcpo_thms' = map (Thm.transfer thy) pcpo_thms
     fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms')
@@ -184,7 +184,7 @@
     val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
     val thy = lthy
       |> Class.prove_instantiation_exit
-          (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
+          (K (rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
   in ((info, below_def), thy) end
 
 fun prepare_cpodef
@@ -207,7 +207,7 @@
     fun cpodef_result nonempty admissible thy =
       let
         val ((info as (_, {type_definition, ...}), below_def), thy) = thy
-          |> add_podef typ set opt_morphs (Tactic.rtac nonempty 1)
+          |> add_podef typ set opt_morphs (rtac nonempty 1)
         val (cpo_info, thy) = thy
           |> prove_cpo name newT morphs type_definition below_def admissible
       in
@@ -239,7 +239,7 @@
 
     fun pcpodef_result bottom_mem admissible thy =
       let
-        val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1
+        val tac = rtac exI 1 THEN rtac bottom_mem 1
         val ((info as (_, {type_definition, ...}), below_def), thy) = thy
           |> add_podef typ set opt_morphs tac
         val (cpo_info, thy) = thy
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -167,7 +167,7 @@
       liftemb_def, liftprj_def, liftdefl_def]
     val thy = lthy
       |> Class.prove_instantiation_instance
-          (K (Tactic.rtac (@{thm typedef_domain_class} OF typedef_thms) 1))
+          (K (rtac (@{thm typedef_domain_class} OF typedef_thms) 1))
       |> Local_Theory.exit_global
 
     (*other theorems*)
--- a/src/HOL/Nominal/nominal_induct.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -124,7 +124,7 @@
               (finish_rule (Induct.internalize more_consumes rule)) i st'
             |> Seq.maps (fn rule' =>
               CASES (rule_cases ctxt rule' cases)
-                (Tactic.rtac (rename_params_rule false [] rule') i THEN
+                (rtac (rename_params_rule false [] rule') i THEN
                   PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
     THEN_ALL_NEW_CASES
       ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
--- a/src/HOL/SMT_Examples/boogie.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/SMT_Examples/boogie.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -18,7 +18,7 @@
 
 
 val isabelle_name =
-  let 
+  let
     fun purge s = if Symbol.is_letter s orelse Symbol.is_digit s then s else
       (case s of
         "." => "_o_"
@@ -303,7 +303,7 @@
   let
     val (text, thy') = Thy_Load.use_file (Path.explode file_name) thy
     val lines = explode_lines text
-    
+
     val ((axioms, vc), ctxt) =
       empty_context
       |> parse_lines lines
@@ -312,7 +312,7 @@
 
     val _ = Goal.prove ctxt [] axioms vc (fn {prems, context} =>
       boogie_tac context prems)
-    val _ = Output.writeln "Verification condition proved successfully"
+    val _ = writeln "Verification condition proved successfully"
 
   in thy' end
 
--- a/src/HOL/Tools/Function/termination.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -305,7 +305,7 @@
   in
     (PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
      THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
-     THEN Raw_Simplifier.rewrite_goal_tac Un_aci_simps 1) st  (* eliminate duplicates *)
+     THEN rewrite_goal_tac Un_aci_simps 1) st  (* eliminate duplicates *)
   end
 
 end
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -105,7 +105,7 @@
          so that "Thm.equal_elim" works below. *)
       val t0 $ _ $ t2 = prop_of eq_th
       val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy
-      val eq_th' = Goal.prove_internal [] eq_ct (K (Tactic.rtac eq_th 1))
+      val eq_th' = Goal.prove_internal [] eq_ct (K (rtac eq_th 1))
     in Thm.equal_elim eq_th' th end
 
 fun clause_params ordering =
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -236,7 +236,7 @@
       (PEEK nprems_of
         (fn n =>
           ALLGOALS (fn i =>
-            Simplifier.rewrite_goal_tac [@{thm split_paired_all}] i
+            rewrite_goal_tac [@{thm split_paired_all}] i
             THEN (SUBPROOF (instantiate i n) ctxt i))))
   in
     Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -83,8 +83,7 @@
         let
           val prems' = maps dest_conjunct_prem (take nargs prems)
         in
-          Simplifier.rewrite_goal_tac
-            (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+          rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
         end) ctxt 1
     | Abs _ => raise Fail "prove_param: No valid parameter term"
   in
@@ -169,7 +168,7 @@
                 let
                   val prems' = maps dest_conjunct_prem (take nargs prems)
                 in
-                  Simplifier.rewrite_goal_tac
+                  rewrite_goal_tac
                     (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
                 end
              THEN REPEAT_DETERM (rtac @{thm refl} 1))
@@ -210,8 +209,7 @@
               let
                 val prems' = maps dest_conjunct_prem (take nargs prems)
               in
-                Simplifier.rewrite_goal_tac
-                  (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+                rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
               end) ctxt 1
       THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
     | prove_prems out_ts ((p, deriv) :: ps) =
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -354,12 +354,12 @@
   fun tag_rules thms = map_index (apsnd (pair NONE)) thms
   fun tag_prems thms = map (pair ~1 o pair NONE) thms
 
-  fun resolve (SOME thm) = Tactic.rtac thm 1
+  fun resolve (SOME thm) = rtac thm 1
     | resolve NONE = no_tac
 
   fun tac prove ctxt rules =
     CONVERSION (SMT_Normalize.atomize_conv ctxt)
-    THEN' Tactic.rtac @{thm ccontr}
+    THEN' rtac @{thm ccontr}
     THEN' SUBPROOF (fn {context, prems, ...} =>
       resolve (prove context (tag_rules rules @ tag_prems prems))) ctxt
 in
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -33,7 +33,7 @@
 val prove_ite =
   Z3_Proof_Tools.by_tac (
     CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv))
-    THEN' Tactic.rtac @{thm refl})
+    THEN' rtac @{thm refl})
 
 
 
@@ -71,7 +71,7 @@
     val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
   in
     Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
-    |> apply (Tactic.rtac @{thm injI})
+    |> apply (rtac @{thm injI})
     |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}])
     |> Goal.norm_result o Goal.finish ctxt'
     |> singleton (Variable.export ctxt' ctxt)
@@ -80,8 +80,8 @@
 fun prove_rhs ctxt def lhs =
   Z3_Proof_Tools.by_tac (
     CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
-    THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI})
-    THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
+    THEN' REPEAT_ALL_NEW (match_tac @{thms allI})
+    THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
 
 
 fun expand thm ct =
@@ -142,7 +142,7 @@
 fun prove_injectivity ctxt =
   Z3_Proof_Tools.by_tac (
     CONVERSION (SMT_Utils.prop_conv (norm_conv ctxt))
-    THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt)))
+    THEN' CSUBGOAL (uncurry (rtac o prove_inj_eq ctxt)))
 
 end
 
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -415,9 +415,9 @@
     @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
 
   fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
-    Tactic.rtac thm ORELSE'
-    (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
-    (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
+    rtac thm ORELSE'
+    (match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
+    (match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
 
   fun nnf_quant_tac_varified vars eq =
     nnf_quant_tac (Z3_Proof_Tools.varify vars eq)
@@ -557,7 +557,7 @@
     val thm = meta_eq_of p
     val rules' = Z3_Proof_Tools.varify vars thm :: rules
     val cu = Z3_Proof_Tools.as_meta_eq ct
-    val tac = REPEAT_ALL_NEW (Tactic.match_tac rules')
+    val tac = REPEAT_ALL_NEW (match_tac rules')
   in MetaEq (Z3_Proof_Tools.by_tac tac cu) end
 end
 
@@ -580,10 +580,10 @@
   val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
 
   fun elim_unused_tac i st = (
-    Tactic.match_tac [@{thm refl}]
-    ORELSE' (Tactic.match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
+    match_tac [@{thm refl}]
+    ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
     ORELSE' (
-      Tactic.match_tac [@{thm iff_allI}, @{thm iff_exI}]
+      match_tac [@{thm iff_allI}, @{thm iff_exI}]
       THEN' elim_unused_tac)) i st
 in
 
@@ -603,8 +603,8 @@
   val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
 in
 val quant_inst = Thm o Z3_Proof_Tools.by_tac (
-  REPEAT_ALL_NEW (Tactic.match_tac [rule])
-  THEN' Tactic.rtac @{thm excluded_middle})
+  REPEAT_ALL_NEW (match_tac [rule])
+  THEN' rtac @{thm excluded_middle})
 end
 
 
@@ -639,10 +639,10 @@
   apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
 
 fun discharge_sk_tac i st = (
-  Tactic.rtac @{thm trans} i
-  THEN Tactic.resolve_tac sk_rules i
-  THEN (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
-  THEN Tactic.rtac @{thm refl} i) st
+  rtac @{thm trans} i
+  THEN resolve_tac sk_rules i
+  THEN (rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
+  THEN rtac @{thm refl} i) st
 
 end
 
@@ -720,14 +720,14 @@
         THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
     Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
       Z3_Proof_Tools.by_tac (
-        (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
+        (rtac @{thm iff_allI} ORELSE' K all_tac)
         THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
         THEN_ALL_NEW (
           NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
           ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
     Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
       Z3_Proof_Tools.by_tac (
-        (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
+        (rtac @{thm iff_allI} ORELSE' K all_tac)
         THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
         THEN_ALL_NEW (
           NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
@@ -736,7 +736,7 @@
     Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
       (fn ctxt' =>
         Z3_Proof_Tools.by_tac (
-          (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
+          (rtac @{thm iff_allI} ORELSE' K all_tac)
           THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
           THEN_ALL_NEW (
             NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
@@ -856,8 +856,7 @@
     @{thm reflexive}, Z3_Proof_Literals.true_thm]
 
   fun discharge_assms_tac rules =
-    REPEAT (HEADGOAL (
-      Tactic.resolve_tac rules ORELSE' SOLVED' discharge_sk_tac))
+    REPEAT (HEADGOAL (resolve_tac rules ORELSE' SOLVED' discharge_sk_tac))
     
   fun discharge_assms rules thm =
     if Thm.nprems_of thm = 0 then Goal.norm_result thm
--- a/src/HOL/Tools/inductive.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/HOL/Tools/inductive.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -533,7 +533,7 @@
 val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
   (fn _ => assume_tac 1);
 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
-val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
+val elim_tac = REPEAT o eresolve_tac elim_rls;
 
 fun simp_case_tac ctxt i =
   EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
--- a/src/Provers/classical.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Provers/classical.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -158,7 +158,7 @@
       val rule'' =
         rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
           if i = 1 orelse redundant_hyp goal
-          then Tactic.etac thin_rl i
+          then etac thin_rl i
           else all_tac))
         |> Seq.hd
         |> Drule.zero_var_indexes;
@@ -897,9 +897,9 @@
     val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
     val rules = rules1 @ rules2 @ rules3 @ rules4;
     val ruleq = Drule.multi_resolves facts rules;
+    val _ = Method.trace ctxt rules;
   in
-    Method.trace ctxt rules;
-    fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq
+    fn st => Seq.maps (fn rule => rtac rule i st) ruleq
   end)
   THEN_ALL_NEW Goal.norm_hhf_tac;
 
--- a/src/Pure/Isar/class.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/class.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -252,7 +252,7 @@
         (fst o rules thy) sub];
     val classrel =
       Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
-        (K (EVERY (map (TRYALL o Tactic.rtac) intros)));
+        (K (EVERY (map (TRYALL o rtac) intros)));
     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub])
       |> filter (is_class thy);
--- a/src/Pure/Isar/class_declaration.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -56,7 +56,7 @@
         val loc_intro_tac =
           (case Locale.intros_of thy class of
             (_, NONE) => all_tac
-          | (_, SOME intro) => ALLGOALS (Tactic.rtac intro));
+          | (_, SOME intro) => ALLGOALS (rtac intro));
         val tac = loc_intro_tac
           THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom));
       in Element.prove_witness empty_ctxt prop tac end) some_prop;
@@ -94,8 +94,8 @@
     val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
     val tac =
       REPEAT (SOMEGOAL
-        (Tactic.match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
-          ORELSE' Tactic.assume_tac));
+        (match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
+          ORELSE' assume_tac));
     val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (K tac);
 
   in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
--- a/src/Pure/Isar/element.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/element.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -262,17 +262,16 @@
 fun transform_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
 
 fun prove_witness ctxt t tac =
-  Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ =>
-    Tactic.rtac Drule.protectI 1 THEN tac)));
+  Witness (t,
+    Thm.close_derivation
+      (Goal.prove ctxt [] [] (mark_witness t) (fn _ => rtac Drule.protectI 1 THEN tac)));
 
 
 local
 
 val refine_witness =
   Proof.refine (Method.Basic (K (RAW_METHOD
-    (K (ALLGOALS
-      (CONJUNCTS (ALLGOALS
-        (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI))))))))));
+    (K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI))))))))));
 
 fun gen_witness_proof proof after_qed wit_propss eq_props =
   let
--- a/src/Pure/Isar/expression.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/expression.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -666,17 +666,15 @@
 
     val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
       rewrite_goals_tac [pred_def] THEN
-      Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
-      Tactic.compose_tac (false,
-        Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
+      compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
+      compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
       |> Conjunction.elim_balanced (length ts);
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
       Element.prove_witness defs_ctxt t
-       (rewrite_goals_tac defs THEN
-        Tactic.compose_tac (false, ax, 0) 1));
+       (rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1));
   in ((statement, intro, axioms), defs_thy) end;
 
 in
--- a/src/Pure/Isar/method.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/method.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -108,7 +108,7 @@
 local
 
 fun cut_rule_tac rule =
-  Tactic.rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
+  rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
 
 in
 
@@ -135,8 +135,8 @@
 
 (* unfold intro/elim rules *)
 
-fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths));
-fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths));
+fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ths));
+fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ths));
 
 
 (* unfold/fold definitions *)
@@ -153,7 +153,7 @@
 
 (* this -- resolve facts directly *)
 
-val this = METHOD (EVERY o map (HEADGOAL o Tactic.rtac));
+val this = METHOD (EVERY o map (HEADGOAL o rtac));
 
 
 (* fact -- composition by facts from context *)
@@ -168,7 +168,7 @@
 
 fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
   if cond (Logic.strip_assums_concl prop)
-  then Tactic.rtac rule i else no_tac);
+  then rtac rule i else no_tac);
 
 in
 
@@ -215,7 +215,7 @@
   THEN_ALL_NEW Goal.norm_hhf_tac;
 
 fun gen_arule_tac tac j rules facts =
-  EVERY' (gen_rule_tac tac rules facts :: replicate j Tactic.assume_tac);
+  EVERY' (gen_rule_tac tac rules facts :: replicate j assume_tac);
 
 fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) =>
   let
@@ -229,14 +229,14 @@
 
 in
 
-val rule_tac = gen_rule_tac Tactic.resolve_tac;
+val rule_tac = gen_rule_tac resolve_tac;
 val rule = meth rule_tac;
 val some_rule_tac = gen_some_rule_tac rule_tac;
 val some_rule = meth' some_rule_tac;
 
-val erule = meth' (gen_arule_tac Tactic.eresolve_tac);
-val drule = meth' (gen_arule_tac Tactic.dresolve_tac);
-val frule = meth' (gen_arule_tac Tactic.forward_tac);
+val erule = meth' (gen_arule_tac eresolve_tac);
+val drule = meth' (gen_arule_tac dresolve_tac);
+val frule = meth' (gen_arule_tac forward_tac);
 
 end;
 
@@ -461,10 +461,10 @@
   setup (Binding.name "assumption") (Scan.succeed assumption)
     "proof by assumption, preferring facts" #>
   setup (Binding.name "rename_tac") (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
-    (fn (quant, xs) => K (SIMPLE_METHOD'' quant (Tactic.rename_tac xs))))
+    (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) >>
-    (fn (quant, i) => K (SIMPLE_METHOD'' quant (Tactic.rotate_tac i))))
+    (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)
     "ML tactic as proof method" #>
--- a/src/Pure/Isar/proof.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -446,12 +446,12 @@
       Goal.norm_hhf_tac THEN'
       SUBGOAL (fn (goal, i) =>
         if can Logic.unprotect (Logic.strip_assums_concl goal) then
-          Tactic.etac Drule.protectI i THEN finish_tac (n - 1) i
+          etac Drule.protectI i THEN finish_tac (n - 1) i
         else finish_tac (n - 1) (i + 1));
 
 fun goal_tac rule =
   Goal.norm_hhf_tac THEN'
-  Tactic.rtac rule THEN'
+  rtac rule THEN'
   finish_tac (Thm.nprems_of rule);
 
 fun FINDGOAL tac st =
--- a/src/Pure/Isar/rule_insts.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -332,11 +332,11 @@
         [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
       | _ => error "Cannot have instantiations with multiple rules")));
 
-val res_inst_meth = method res_inst_tac (K Tactic.resolve_tac);
-val eres_inst_meth = method eres_inst_tac (K Tactic.eresolve_tac);
-val cut_inst_meth = method cut_inst_tac (K Tactic.cut_rules_tac);
-val dres_inst_meth = method dres_inst_tac (K Tactic.dresolve_tac);
-val forw_inst_meth = method forw_inst_tac (K Tactic.forward_tac);
+val res_inst_meth = method res_inst_tac (K resolve_tac);
+val eres_inst_meth = method eres_inst_tac (K eresolve_tac);
+val cut_inst_meth = method cut_inst_tac (K cut_rules_tac);
+val dres_inst_meth = method dres_inst_tac (K dresolve_tac);
+val forw_inst_meth = method forw_inst_tac (K forward_tac);
 
 
 (* setup *)
--- a/src/Pure/goal.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/goal.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -425,7 +425,7 @@
     val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
     val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
     val tacs = Rs |> map (fn R =>
-      Tactic.etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
+      etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
   in fold_rev (curry op APPEND') tacs (K no_tac) i end);
 
 
--- a/src/Tools/case_product.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Tools/case_product.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -70,10 +70,9 @@
     val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
     val thm2' = thm2 OF p_cons2
   in
-    Tactic.rtac (thm1 OF p_cons1)
+    rtac (thm1 OF p_cons1)
      THEN' EVERY' (map (fn p =>
-       Tactic.rtac thm2'
-       THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
+       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
   end
 
 fun combine ctxt thm1 thm2 =
--- a/src/Tools/eqsubst.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Tools/eqsubst.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -252,7 +252,7 @@
   RW_Inst.rw ctxt m rule conclthm
   |> unfix_frees cfvs
   |> Conv.fconv_rule Drule.beta_eta_conversion
-  |> (fn r => Tactic.rtac r i st);
+  |> (fn r => rtac r i st);
 
 (* substitute within the conclusion of goal i of gth, using a meta
 equation rule. Note that we assume rule has var indicies zero'd *)
@@ -334,8 +334,7 @@
       |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
   in
     (* ~j because new asm starts at back, thus we subtract 1 *)
-    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))
-      (Tactic.dtac preelimrule i st2)
+    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dtac preelimrule i st2)
   end;
 
 
--- a/src/Tools/induct.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Tools/induct.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -534,10 +534,10 @@
 
 val atomize_cterm = Raw_Simplifier.rewrite true Induct_Args.atomize;
 
-val atomize_tac = Simplifier.rewrite_goal_tac Induct_Args.atomize;
+val atomize_tac = rewrite_goal_tac Induct_Args.atomize;
 
 val inner_atomize_tac =
-  Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
+  rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
 
 
 (* rulify *)
@@ -554,10 +554,10 @@
   in (thy, Logic.list_implies (map rulify As, rulify B)) end;
 
 val rulify_tac =
-  Simplifier.rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
-  Simplifier.rewrite_goal_tac Induct_Args.rulify_fallback THEN'
+  rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
+  rewrite_goal_tac Induct_Args.rulify_fallback THEN'
   Goal.conjunction_tac THEN_ALL_NEW
-  (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
+  (rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
 
 
 (* prepare rule *)
--- a/src/Tools/intuitionistic.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Tools/intuitionistic.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -20,7 +20,7 @@
 val remdups_tac = SUBGOAL (fn (g, i) =>
   let val prems = Logic.strip_assums_hyp g in
     REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
-    (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
+    (ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
   end);
 
 fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;