standardized aliases;
authorwenzelm
Sat Jul 27 16:35:51 2013 +0200 (2013-07-27)
changeset 52732b4da1f2ec73f
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
     1.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Thu Jul 25 16:46:53 2013 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Sat Jul 27 16:35:51 2013 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4      val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible]
     1.5      val (full_tname, Ts) = dest_Type newT
     1.6      val lhs_sorts = map (snd o dest_TFree) Ts
     1.7 -    val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1
     1.8 +    val tac = rtac (@{thm typedef_cpo} OF cpo_thms) 1
     1.9      val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy
    1.10      (* transfer thms so that they will know about the new cpo instance *)
    1.11      val cpo_thms' = map (Thm.transfer thy) cpo_thms
    1.12 @@ -112,7 +112,7 @@
    1.13      val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem]
    1.14      val (full_tname, Ts) = dest_Type newT
    1.15      val lhs_sorts = map (snd o dest_TFree) Ts
    1.16 -    val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
    1.17 +    val tac = rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
    1.18      val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy
    1.19      val pcpo_thms' = map (Thm.transfer thy) pcpo_thms
    1.20      fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms')
    1.21 @@ -184,7 +184,7 @@
    1.22      val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
    1.23      val thy = lthy
    1.24        |> Class.prove_instantiation_exit
    1.25 -          (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
    1.26 +          (K (rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
    1.27    in ((info, below_def), thy) end
    1.28  
    1.29  fun prepare_cpodef
    1.30 @@ -207,7 +207,7 @@
    1.31      fun cpodef_result nonempty admissible thy =
    1.32        let
    1.33          val ((info as (_, {type_definition, ...}), below_def), thy) = thy
    1.34 -          |> add_podef typ set opt_morphs (Tactic.rtac nonempty 1)
    1.35 +          |> add_podef typ set opt_morphs (rtac nonempty 1)
    1.36          val (cpo_info, thy) = thy
    1.37            |> prove_cpo name newT morphs type_definition below_def admissible
    1.38        in
    1.39 @@ -239,7 +239,7 @@
    1.40  
    1.41      fun pcpodef_result bottom_mem admissible thy =
    1.42        let
    1.43 -        val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1
    1.44 +        val tac = rtac exI 1 THEN rtac bottom_mem 1
    1.45          val ((info as (_, {type_definition, ...}), below_def), thy) = thy
    1.46            |> add_podef typ set opt_morphs tac
    1.47          val (cpo_info, thy) = thy
     2.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Thu Jul 25 16:46:53 2013 +0200
     2.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sat Jul 27 16:35:51 2013 +0200
     2.3 @@ -167,7 +167,7 @@
     2.4        liftemb_def, liftprj_def, liftdefl_def]
     2.5      val thy = lthy
     2.6        |> Class.prove_instantiation_instance
     2.7 -          (K (Tactic.rtac (@{thm typedef_domain_class} OF typedef_thms) 1))
     2.8 +          (K (rtac (@{thm typedef_domain_class} OF typedef_thms) 1))
     2.9        |> Local_Theory.exit_global
    2.10  
    2.11      (*other theorems*)
     3.1 --- a/src/HOL/Nominal/nominal_induct.ML	Thu Jul 25 16:46:53 2013 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sat Jul 27 16:35:51 2013 +0200
     3.3 @@ -124,7 +124,7 @@
     3.4                (finish_rule (Induct.internalize more_consumes rule)) i st'
     3.5              |> Seq.maps (fn rule' =>
     3.6                CASES (rule_cases ctxt rule' cases)
     3.7 -                (Tactic.rtac (rename_params_rule false [] rule') i THEN
     3.8 +                (rtac (rename_params_rule false [] rule') i THEN
     3.9                    PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
    3.10      THEN_ALL_NEW_CASES
    3.11        ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
     4.1 --- a/src/HOL/SMT_Examples/boogie.ML	Thu Jul 25 16:46:53 2013 +0200
     4.2 +++ b/src/HOL/SMT_Examples/boogie.ML	Sat Jul 27 16:35:51 2013 +0200
     4.3 @@ -18,7 +18,7 @@
     4.4  
     4.5  
     4.6  val isabelle_name =
     4.7 -  let 
     4.8 +  let
     4.9      fun purge s = if Symbol.is_letter s orelse Symbol.is_digit s then s else
    4.10        (case s of
    4.11          "." => "_o_"
    4.12 @@ -303,7 +303,7 @@
    4.13    let
    4.14      val (text, thy') = Thy_Load.use_file (Path.explode file_name) thy
    4.15      val lines = explode_lines text
    4.16 -    
    4.17 +
    4.18      val ((axioms, vc), ctxt) =
    4.19        empty_context
    4.20        |> parse_lines lines
    4.21 @@ -312,7 +312,7 @@
    4.22  
    4.23      val _ = Goal.prove ctxt [] axioms vc (fn {prems, context} =>
    4.24        boogie_tac context prems)
    4.25 -    val _ = Output.writeln "Verification condition proved successfully"
    4.26 +    val _ = writeln "Verification condition proved successfully"
    4.27  
    4.28    in thy' end
    4.29  
     5.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Jul 25 16:46:53 2013 +0200
     5.2 +++ b/src/HOL/Tools/Function/termination.ML	Sat Jul 27 16:35:51 2013 +0200
     5.3 @@ -305,7 +305,7 @@
     5.4    in
     5.5      (PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
     5.6       THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
     5.7 -     THEN Raw_Simplifier.rewrite_goal_tac Un_aci_simps 1) st  (* eliminate duplicates *)
     5.8 +     THEN rewrite_goal_tac Un_aci_simps 1) st  (* eliminate duplicates *)
     5.9    end
    5.10  
    5.11  end
     6.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jul 25 16:46:53 2013 +0200
     6.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Sat Jul 27 16:35:51 2013 +0200
     6.3 @@ -105,7 +105,7 @@
     6.4           so that "Thm.equal_elim" works below. *)
     6.5        val t0 $ _ $ t2 = prop_of eq_th
     6.6        val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy
     6.7 -      val eq_th' = Goal.prove_internal [] eq_ct (K (Tactic.rtac eq_th 1))
     6.8 +      val eq_th' = Goal.prove_internal [] eq_ct (K (rtac eq_th 1))
     6.9      in Thm.equal_elim eq_th' th end
    6.10  
    6.11  fun clause_params ordering =
     7.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Thu Jul 25 16:46:53 2013 +0200
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Sat Jul 27 16:35:51 2013 +0200
     7.3 @@ -236,7 +236,7 @@
     7.4        (PEEK nprems_of
     7.5          (fn n =>
     7.6            ALLGOALS (fn i =>
     7.7 -            Simplifier.rewrite_goal_tac [@{thm split_paired_all}] i
     7.8 +            rewrite_goal_tac [@{thm split_paired_all}] i
     7.9              THEN (SUBPROOF (instantiate i n) ctxt i))))
    7.10    in
    7.11      Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
     8.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu Jul 25 16:46:53 2013 +0200
     8.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sat Jul 27 16:35:51 2013 +0200
     8.3 @@ -83,8 +83,7 @@
     8.4          let
     8.5            val prems' = maps dest_conjunct_prem (take nargs prems)
     8.6          in
     8.7 -          Simplifier.rewrite_goal_tac
     8.8 -            (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
     8.9 +          rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    8.10          end) ctxt 1
    8.11      | Abs _ => raise Fail "prove_param: No valid parameter term"
    8.12    in
    8.13 @@ -169,7 +168,7 @@
    8.14                  let
    8.15                    val prems' = maps dest_conjunct_prem (take nargs prems)
    8.16                  in
    8.17 -                  Simplifier.rewrite_goal_tac
    8.18 +                  rewrite_goal_tac
    8.19                      (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    8.20                  end
    8.21               THEN REPEAT_DETERM (rtac @{thm refl} 1))
    8.22 @@ -210,8 +209,7 @@
    8.23                let
    8.24                  val prems' = maps dest_conjunct_prem (take nargs prems)
    8.25                in
    8.26 -                Simplifier.rewrite_goal_tac
    8.27 -                  (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    8.28 +                rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    8.29                end) ctxt 1
    8.30        THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
    8.31      | prove_prems out_ts ((p, deriv) :: ps) =
     9.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Jul 25 16:46:53 2013 +0200
     9.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Sat Jul 27 16:35:51 2013 +0200
     9.3 @@ -354,12 +354,12 @@
     9.4    fun tag_rules thms = map_index (apsnd (pair NONE)) thms
     9.5    fun tag_prems thms = map (pair ~1 o pair NONE) thms
     9.6  
     9.7 -  fun resolve (SOME thm) = Tactic.rtac thm 1
     9.8 +  fun resolve (SOME thm) = rtac thm 1
     9.9      | resolve NONE = no_tac
    9.10  
    9.11    fun tac prove ctxt rules =
    9.12      CONVERSION (SMT_Normalize.atomize_conv ctxt)
    9.13 -    THEN' Tactic.rtac @{thm ccontr}
    9.14 +    THEN' rtac @{thm ccontr}
    9.15      THEN' SUBPROOF (fn {context, prems, ...} =>
    9.16        resolve (prove context (tag_rules rules @ tag_prems prems))) ctxt
    9.17  in
    10.1 --- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Thu Jul 25 16:46:53 2013 +0200
    10.2 +++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Sat Jul 27 16:35:51 2013 +0200
    10.3 @@ -33,7 +33,7 @@
    10.4  val prove_ite =
    10.5    Z3_Proof_Tools.by_tac (
    10.6      CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv))
    10.7 -    THEN' Tactic.rtac @{thm refl})
    10.8 +    THEN' rtac @{thm refl})
    10.9  
   10.10  
   10.11  
   10.12 @@ -71,7 +71,7 @@
   10.13      val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
   10.14    in
   10.15      Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
   10.16 -    |> apply (Tactic.rtac @{thm injI})
   10.17 +    |> apply (rtac @{thm injI})
   10.18      |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}])
   10.19      |> Goal.norm_result o Goal.finish ctxt'
   10.20      |> singleton (Variable.export ctxt' ctxt)
   10.21 @@ -80,8 +80,8 @@
   10.22  fun prove_rhs ctxt def lhs =
   10.23    Z3_Proof_Tools.by_tac (
   10.24      CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
   10.25 -    THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI})
   10.26 -    THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
   10.27 +    THEN' REPEAT_ALL_NEW (match_tac @{thms allI})
   10.28 +    THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
   10.29  
   10.30  
   10.31  fun expand thm ct =
   10.32 @@ -142,7 +142,7 @@
   10.33  fun prove_injectivity ctxt =
   10.34    Z3_Proof_Tools.by_tac (
   10.35      CONVERSION (SMT_Utils.prop_conv (norm_conv ctxt))
   10.36 -    THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt)))
   10.37 +    THEN' CSUBGOAL (uncurry (rtac o prove_inj_eq ctxt)))
   10.38  
   10.39  end
   10.40  
    11.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu Jul 25 16:46:53 2013 +0200
    11.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat Jul 27 16:35:51 2013 +0200
    11.3 @@ -415,9 +415,9 @@
    11.4      @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
    11.5  
    11.6    fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
    11.7 -    Tactic.rtac thm ORELSE'
    11.8 -    (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
    11.9 -    (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
   11.10 +    rtac thm ORELSE'
   11.11 +    (match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
   11.12 +    (match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
   11.13  
   11.14    fun nnf_quant_tac_varified vars eq =
   11.15      nnf_quant_tac (Z3_Proof_Tools.varify vars eq)
   11.16 @@ -557,7 +557,7 @@
   11.17      val thm = meta_eq_of p
   11.18      val rules' = Z3_Proof_Tools.varify vars thm :: rules
   11.19      val cu = Z3_Proof_Tools.as_meta_eq ct
   11.20 -    val tac = REPEAT_ALL_NEW (Tactic.match_tac rules')
   11.21 +    val tac = REPEAT_ALL_NEW (match_tac rules')
   11.22    in MetaEq (Z3_Proof_Tools.by_tac tac cu) end
   11.23  end
   11.24  
   11.25 @@ -580,10 +580,10 @@
   11.26    val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
   11.27  
   11.28    fun elim_unused_tac i st = (
   11.29 -    Tactic.match_tac [@{thm refl}]
   11.30 -    ORELSE' (Tactic.match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
   11.31 +    match_tac [@{thm refl}]
   11.32 +    ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
   11.33      ORELSE' (
   11.34 -      Tactic.match_tac [@{thm iff_allI}, @{thm iff_exI}]
   11.35 +      match_tac [@{thm iff_allI}, @{thm iff_exI}]
   11.36        THEN' elim_unused_tac)) i st
   11.37  in
   11.38  
   11.39 @@ -603,8 +603,8 @@
   11.40    val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
   11.41  in
   11.42  val quant_inst = Thm o Z3_Proof_Tools.by_tac (
   11.43 -  REPEAT_ALL_NEW (Tactic.match_tac [rule])
   11.44 -  THEN' Tactic.rtac @{thm excluded_middle})
   11.45 +  REPEAT_ALL_NEW (match_tac [rule])
   11.46 +  THEN' rtac @{thm excluded_middle})
   11.47  end
   11.48  
   11.49  
   11.50 @@ -639,10 +639,10 @@
   11.51    apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
   11.52  
   11.53  fun discharge_sk_tac i st = (
   11.54 -  Tactic.rtac @{thm trans} i
   11.55 -  THEN Tactic.resolve_tac sk_rules i
   11.56 -  THEN (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
   11.57 -  THEN Tactic.rtac @{thm refl} i) st
   11.58 +  rtac @{thm trans} i
   11.59 +  THEN resolve_tac sk_rules i
   11.60 +  THEN (rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
   11.61 +  THEN rtac @{thm refl} i) st
   11.62  
   11.63  end
   11.64  
   11.65 @@ -720,14 +720,14 @@
   11.66          THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
   11.67      Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
   11.68        Z3_Proof_Tools.by_tac (
   11.69 -        (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
   11.70 +        (rtac @{thm iff_allI} ORELSE' K all_tac)
   11.71          THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
   11.72          THEN_ALL_NEW (
   11.73            NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
   11.74            ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
   11.75      Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
   11.76        Z3_Proof_Tools.by_tac (
   11.77 -        (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
   11.78 +        (rtac @{thm iff_allI} ORELSE' K all_tac)
   11.79          THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
   11.80          THEN_ALL_NEW (
   11.81            NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
   11.82 @@ -736,7 +736,7 @@
   11.83      Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
   11.84        (fn ctxt' =>
   11.85          Z3_Proof_Tools.by_tac (
   11.86 -          (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
   11.87 +          (rtac @{thm iff_allI} ORELSE' K all_tac)
   11.88            THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
   11.89            THEN_ALL_NEW (
   11.90              NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
   11.91 @@ -856,8 +856,7 @@
   11.92      @{thm reflexive}, Z3_Proof_Literals.true_thm]
   11.93  
   11.94    fun discharge_assms_tac rules =
   11.95 -    REPEAT (HEADGOAL (
   11.96 -      Tactic.resolve_tac rules ORELSE' SOLVED' discharge_sk_tac))
   11.97 +    REPEAT (HEADGOAL (resolve_tac rules ORELSE' SOLVED' discharge_sk_tac))
   11.98      
   11.99    fun discharge_assms rules thm =
  11.100      if Thm.nprems_of thm = 0 then Goal.norm_result thm
    12.1 --- a/src/HOL/Tools/inductive.ML	Thu Jul 25 16:46:53 2013 +0200
    12.2 +++ b/src/HOL/Tools/inductive.ML	Sat Jul 27 16:35:51 2013 +0200
    12.3 @@ -533,7 +533,7 @@
    12.4  val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
    12.5    (fn _ => assume_tac 1);
    12.6  val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
    12.7 -val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
    12.8 +val elim_tac = REPEAT o eresolve_tac elim_rls;
    12.9  
   12.10  fun simp_case_tac ctxt i =
   12.11    EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
    13.1 --- a/src/Provers/classical.ML	Thu Jul 25 16:46:53 2013 +0200
    13.2 +++ b/src/Provers/classical.ML	Sat Jul 27 16:35:51 2013 +0200
    13.3 @@ -158,7 +158,7 @@
    13.4        val rule'' =
    13.5          rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
    13.6            if i = 1 orelse redundant_hyp goal
    13.7 -          then Tactic.etac thin_rl i
    13.8 +          then etac thin_rl i
    13.9            else all_tac))
   13.10          |> Seq.hd
   13.11          |> Drule.zero_var_indexes;
   13.12 @@ -897,9 +897,9 @@
   13.13      val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
   13.14      val rules = rules1 @ rules2 @ rules3 @ rules4;
   13.15      val ruleq = Drule.multi_resolves facts rules;
   13.16 +    val _ = Method.trace ctxt rules;
   13.17    in
   13.18 -    Method.trace ctxt rules;
   13.19 -    fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq
   13.20 +    fn st => Seq.maps (fn rule => rtac rule i st) ruleq
   13.21    end)
   13.22    THEN_ALL_NEW Goal.norm_hhf_tac;
   13.23  
    14.1 --- a/src/Pure/Isar/class.ML	Thu Jul 25 16:46:53 2013 +0200
    14.2 +++ b/src/Pure/Isar/class.ML	Sat Jul 27 16:35:51 2013 +0200
    14.3 @@ -252,7 +252,7 @@
    14.4          (fst o rules thy) sub];
    14.5      val classrel =
    14.6        Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
    14.7 -        (K (EVERY (map (TRYALL o Tactic.rtac) intros)));
    14.8 +        (K (EVERY (map (TRYALL o rtac) intros)));
    14.9      val diff_sort = Sign.complete_sort thy [sup]
   14.10        |> subtract (op =) (Sign.complete_sort thy [sub])
   14.11        |> filter (is_class thy);
    15.1 --- a/src/Pure/Isar/class_declaration.ML	Thu Jul 25 16:46:53 2013 +0200
    15.2 +++ b/src/Pure/Isar/class_declaration.ML	Sat Jul 27 16:35:51 2013 +0200
    15.3 @@ -56,7 +56,7 @@
    15.4          val loc_intro_tac =
    15.5            (case Locale.intros_of thy class of
    15.6              (_, NONE) => all_tac
    15.7 -          | (_, SOME intro) => ALLGOALS (Tactic.rtac intro));
    15.8 +          | (_, SOME intro) => ALLGOALS (rtac intro));
    15.9          val tac = loc_intro_tac
   15.10            THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom));
   15.11        in Element.prove_witness empty_ctxt prop tac end) some_prop;
   15.12 @@ -94,8 +94,8 @@
   15.13      val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
   15.14      val tac =
   15.15        REPEAT (SOMEGOAL
   15.16 -        (Tactic.match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
   15.17 -          ORELSE' Tactic.assume_tac));
   15.18 +        (match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
   15.19 +          ORELSE' assume_tac));
   15.20      val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (K tac);
   15.21  
   15.22    in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
    16.1 --- a/src/Pure/Isar/element.ML	Thu Jul 25 16:46:53 2013 +0200
    16.2 +++ b/src/Pure/Isar/element.ML	Sat Jul 27 16:35:51 2013 +0200
    16.3 @@ -262,17 +262,16 @@
    16.4  fun transform_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
    16.5  
    16.6  fun prove_witness ctxt t tac =
    16.7 -  Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ =>
    16.8 -    Tactic.rtac Drule.protectI 1 THEN tac)));
    16.9 +  Witness (t,
   16.10 +    Thm.close_derivation
   16.11 +      (Goal.prove ctxt [] [] (mark_witness t) (fn _ => rtac Drule.protectI 1 THEN tac)));
   16.12  
   16.13  
   16.14  local
   16.15  
   16.16  val refine_witness =
   16.17    Proof.refine (Method.Basic (K (RAW_METHOD
   16.18 -    (K (ALLGOALS
   16.19 -      (CONJUNCTS (ALLGOALS
   16.20 -        (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI))))))))));
   16.21 +    (K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI))))))))));
   16.22  
   16.23  fun gen_witness_proof proof after_qed wit_propss eq_props =
   16.24    let
    17.1 --- a/src/Pure/Isar/expression.ML	Thu Jul 25 16:46:53 2013 +0200
    17.2 +++ b/src/Pure/Isar/expression.ML	Sat Jul 27 16:35:51 2013 +0200
    17.3 @@ -666,17 +666,15 @@
    17.4  
    17.5      val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
    17.6        rewrite_goals_tac [pred_def] THEN
    17.7 -      Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
    17.8 -      Tactic.compose_tac (false,
    17.9 -        Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
   17.10 +      compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
   17.11 +      compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
   17.12  
   17.13      val conjuncts =
   17.14        (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
   17.15        |> Conjunction.elim_balanced (length ts);
   17.16      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
   17.17        Element.prove_witness defs_ctxt t
   17.18 -       (rewrite_goals_tac defs THEN
   17.19 -        Tactic.compose_tac (false, ax, 0) 1));
   17.20 +       (rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1));
   17.21    in ((statement, intro, axioms), defs_thy) end;
   17.22  
   17.23  in
    18.1 --- a/src/Pure/Isar/method.ML	Thu Jul 25 16:46:53 2013 +0200
    18.2 +++ b/src/Pure/Isar/method.ML	Sat Jul 27 16:35:51 2013 +0200
    18.3 @@ -108,7 +108,7 @@
    18.4  local
    18.5  
    18.6  fun cut_rule_tac rule =
    18.7 -  Tactic.rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
    18.8 +  rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
    18.9  
   18.10  in
   18.11  
   18.12 @@ -135,8 +135,8 @@
   18.13  
   18.14  (* unfold intro/elim rules *)
   18.15  
   18.16 -fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths));
   18.17 -fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths));
   18.18 +fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ths));
   18.19 +fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ths));
   18.20  
   18.21  
   18.22  (* unfold/fold definitions *)
   18.23 @@ -153,7 +153,7 @@
   18.24  
   18.25  (* this -- resolve facts directly *)
   18.26  
   18.27 -val this = METHOD (EVERY o map (HEADGOAL o Tactic.rtac));
   18.28 +val this = METHOD (EVERY o map (HEADGOAL o rtac));
   18.29  
   18.30  
   18.31  (* fact -- composition by facts from context *)
   18.32 @@ -168,7 +168,7 @@
   18.33  
   18.34  fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
   18.35    if cond (Logic.strip_assums_concl prop)
   18.36 -  then Tactic.rtac rule i else no_tac);
   18.37 +  then rtac rule i else no_tac);
   18.38  
   18.39  in
   18.40  
   18.41 @@ -215,7 +215,7 @@
   18.42    THEN_ALL_NEW Goal.norm_hhf_tac;
   18.43  
   18.44  fun gen_arule_tac tac j rules facts =
   18.45 -  EVERY' (gen_rule_tac tac rules facts :: replicate j Tactic.assume_tac);
   18.46 +  EVERY' (gen_rule_tac tac rules facts :: replicate j assume_tac);
   18.47  
   18.48  fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) =>
   18.49    let
   18.50 @@ -229,14 +229,14 @@
   18.51  
   18.52  in
   18.53  
   18.54 -val rule_tac = gen_rule_tac Tactic.resolve_tac;
   18.55 +val rule_tac = gen_rule_tac resolve_tac;
   18.56  val rule = meth rule_tac;
   18.57  val some_rule_tac = gen_some_rule_tac rule_tac;
   18.58  val some_rule = meth' some_rule_tac;
   18.59  
   18.60 -val erule = meth' (gen_arule_tac Tactic.eresolve_tac);
   18.61 -val drule = meth' (gen_arule_tac Tactic.dresolve_tac);
   18.62 -val frule = meth' (gen_arule_tac Tactic.forward_tac);
   18.63 +val erule = meth' (gen_arule_tac eresolve_tac);
   18.64 +val drule = meth' (gen_arule_tac dresolve_tac);
   18.65 +val frule = meth' (gen_arule_tac forward_tac);
   18.66  
   18.67  end;
   18.68  
   18.69 @@ -461,10 +461,10 @@
   18.70    setup (Binding.name "assumption") (Scan.succeed assumption)
   18.71      "proof by assumption, preferring facts" #>
   18.72    setup (Binding.name "rename_tac") (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
   18.73 -    (fn (quant, xs) => K (SIMPLE_METHOD'' quant (Tactic.rename_tac xs))))
   18.74 +    (fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs))))
   18.75      "rename parameters of goal" #>
   18.76    setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
   18.77 -    (fn (quant, i) => K (SIMPLE_METHOD'' quant (Tactic.rotate_tac i))))
   18.78 +    (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
   18.79        "rotate assumptions of goal" #>
   18.80    setup (Binding.name "tactic") (Scan.lift Args.name_source_position >> tactic)
   18.81      "ML tactic as proof method" #>
    19.1 --- a/src/Pure/Isar/proof.ML	Thu Jul 25 16:46:53 2013 +0200
    19.2 +++ b/src/Pure/Isar/proof.ML	Sat Jul 27 16:35:51 2013 +0200
    19.3 @@ -446,12 +446,12 @@
    19.4        Goal.norm_hhf_tac THEN'
    19.5        SUBGOAL (fn (goal, i) =>
    19.6          if can Logic.unprotect (Logic.strip_assums_concl goal) then
    19.7 -          Tactic.etac Drule.protectI i THEN finish_tac (n - 1) i
    19.8 +          etac Drule.protectI i THEN finish_tac (n - 1) i
    19.9          else finish_tac (n - 1) (i + 1));
   19.10  
   19.11  fun goal_tac rule =
   19.12    Goal.norm_hhf_tac THEN'
   19.13 -  Tactic.rtac rule THEN'
   19.14 +  rtac rule THEN'
   19.15    finish_tac (Thm.nprems_of rule);
   19.16  
   19.17  fun FINDGOAL tac st =
    20.1 --- a/src/Pure/Isar/rule_insts.ML	Thu Jul 25 16:46:53 2013 +0200
    20.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat Jul 27 16:35:51 2013 +0200
    20.3 @@ -332,11 +332,11 @@
    20.4          [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
    20.5        | _ => error "Cannot have instantiations with multiple rules")));
    20.6  
    20.7 -val res_inst_meth = method res_inst_tac (K Tactic.resolve_tac);
    20.8 -val eres_inst_meth = method eres_inst_tac (K Tactic.eresolve_tac);
    20.9 -val cut_inst_meth = method cut_inst_tac (K Tactic.cut_rules_tac);
   20.10 -val dres_inst_meth = method dres_inst_tac (K Tactic.dresolve_tac);
   20.11 -val forw_inst_meth = method forw_inst_tac (K Tactic.forward_tac);
   20.12 +val res_inst_meth = method res_inst_tac (K resolve_tac);
   20.13 +val eres_inst_meth = method eres_inst_tac (K eresolve_tac);
   20.14 +val cut_inst_meth = method cut_inst_tac (K cut_rules_tac);
   20.15 +val dres_inst_meth = method dres_inst_tac (K dresolve_tac);
   20.16 +val forw_inst_meth = method forw_inst_tac (K forward_tac);
   20.17  
   20.18  
   20.19  (* setup *)
    21.1 --- a/src/Pure/goal.ML	Thu Jul 25 16:46:53 2013 +0200
    21.2 +++ b/src/Pure/goal.ML	Sat Jul 27 16:35:51 2013 +0200
    21.3 @@ -425,7 +425,7 @@
    21.4      val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
    21.5      val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
    21.6      val tacs = Rs |> map (fn R =>
    21.7 -      Tactic.etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
    21.8 +      etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
    21.9    in fold_rev (curry op APPEND') tacs (K no_tac) i end);
   21.10  
   21.11  
    22.1 --- a/src/Tools/case_product.ML	Thu Jul 25 16:46:53 2013 +0200
    22.2 +++ b/src/Tools/case_product.ML	Sat Jul 27 16:35:51 2013 +0200
    22.3 @@ -70,10 +70,9 @@
    22.4      val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
    22.5      val thm2' = thm2 OF p_cons2
    22.6    in
    22.7 -    Tactic.rtac (thm1 OF p_cons1)
    22.8 +    rtac (thm1 OF p_cons1)
    22.9       THEN' EVERY' (map (fn p =>
   22.10 -       Tactic.rtac thm2'
   22.11 -       THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
   22.12 +       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
   22.13    end
   22.14  
   22.15  fun combine ctxt thm1 thm2 =
    23.1 --- a/src/Tools/eqsubst.ML	Thu Jul 25 16:46:53 2013 +0200
    23.2 +++ b/src/Tools/eqsubst.ML	Sat Jul 27 16:35:51 2013 +0200
    23.3 @@ -252,7 +252,7 @@
    23.4    RW_Inst.rw ctxt m rule conclthm
    23.5    |> unfix_frees cfvs
    23.6    |> Conv.fconv_rule Drule.beta_eta_conversion
    23.7 -  |> (fn r => Tactic.rtac r i st);
    23.8 +  |> (fn r => rtac r i st);
    23.9  
   23.10  (* substitute within the conclusion of goal i of gth, using a meta
   23.11  equation rule. Note that we assume rule has var indicies zero'd *)
   23.12 @@ -334,8 +334,7 @@
   23.13        |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
   23.14    in
   23.15      (* ~j because new asm starts at back, thus we subtract 1 *)
   23.16 -    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))
   23.17 -      (Tactic.dtac preelimrule i st2)
   23.18 +    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dtac preelimrule i st2)
   23.19    end;
   23.20  
   23.21  
    24.1 --- a/src/Tools/induct.ML	Thu Jul 25 16:46:53 2013 +0200
    24.2 +++ b/src/Tools/induct.ML	Sat Jul 27 16:35:51 2013 +0200
    24.3 @@ -534,10 +534,10 @@
    24.4  
    24.5  val atomize_cterm = Raw_Simplifier.rewrite true Induct_Args.atomize;
    24.6  
    24.7 -val atomize_tac = Simplifier.rewrite_goal_tac Induct_Args.atomize;
    24.8 +val atomize_tac = rewrite_goal_tac Induct_Args.atomize;
    24.9  
   24.10  val inner_atomize_tac =
   24.11 -  Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
   24.12 +  rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
   24.13  
   24.14  
   24.15  (* rulify *)
   24.16 @@ -554,10 +554,10 @@
   24.17    in (thy, Logic.list_implies (map rulify As, rulify B)) end;
   24.18  
   24.19  val rulify_tac =
   24.20 -  Simplifier.rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
   24.21 -  Simplifier.rewrite_goal_tac Induct_Args.rulify_fallback THEN'
   24.22 +  rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
   24.23 +  rewrite_goal_tac Induct_Args.rulify_fallback THEN'
   24.24    Goal.conjunction_tac THEN_ALL_NEW
   24.25 -  (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
   24.26 +  (rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
   24.27  
   24.28  
   24.29  (* prepare rule *)
    25.1 --- a/src/Tools/intuitionistic.ML	Thu Jul 25 16:46:53 2013 +0200
    25.2 +++ b/src/Tools/intuitionistic.ML	Sat Jul 27 16:35:51 2013 +0200
    25.3 @@ -20,7 +20,7 @@
    25.4  val remdups_tac = SUBGOAL (fn (g, i) =>
    25.5    let val prems = Logic.strip_assums_hyp g in
    25.6      REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
    25.7 -    (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
    25.8 +    (ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
    25.9    end);
   25.10  
   25.11  fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;