# HG changeset patch
# User wenzelm
# Date 1414707251 -3600
# Node ID f4bb3068d819f12a719074e7466e4b713e4a23a1
# Parent  773b378d9313520264c571320cd4d73256e83d20# Parent  ccda99401bc8e8f0f54c986f3e8cf4bbf578fbc8
merged

diff -r 773b378d9313 -r f4bb3068d819 src/FOL/ex/Miniscope.thy
--- a/src/FOL/ex/Miniscope.thy	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/FOL/ex/Miniscope.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -65,7 +65,7 @@
 
 ML {*
 val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps});
-fun mini_tac ctxt = rtac @{thm ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
+fun mini_tac ctxt = resolve_tac @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
 *}
 
 end
diff -r 773b378d9313 -r f4bb3068d819 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/FOL/simpdata.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -107,7 +107,9 @@
 val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
 
 fun unsafe_solver ctxt =
-  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), atac, etac @{thm FalseE}];
+  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt),
+    assume_tac,
+    eresolve_tac @{thms FalseE}];
 
 (*No premature instantiation of variables during simplification*)
 fun safe_solver ctxt =
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Fun.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -839,8 +839,8 @@
       | (T, SOME rhs) =>
           SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
             (fn _ =>
-              rtac eq_reflection 1 THEN
-              rtac @{thm ext} 1 THEN
+              resolve_tac [eq_reflection] 1 THEN
+              resolve_tac @{thms ext} 1 THEN
               simp_tac (put_simpset ss ctxt) 1))
     end
 in proc end
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/HOL.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -905,7 +905,7 @@
 apply (rule ex1E [OF major])
 apply (rule prem)
 apply (tactic {* ares_tac @{thms allI} 1 *})+
-apply (tactic {* etac (Classical.dup_elim @{thm allE}) 1 *})
+apply (tactic {* eresolve_tac [Classical.dup_elim @{thm allE}] 1 *})
 apply iprover
 done
 
@@ -1822,7 +1822,7 @@
 proof
   assume "PROP ?ofclass"
   show "PROP ?equal"
-    by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm eq_equal})) *})
+    by (tactic {* ALLGOALS (resolve_tac [Thm.unconstrainT @{thm eq_equal}]) *})
       (fact `PROP ?ofclass`)
 next
   assume "PROP ?equal"
@@ -1921,7 +1921,10 @@
   let
     fun eval_tac ctxt =
       let val conv = Code_Runtime.dynamic_holds_conv ctxt
-      in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
+      in
+        CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
+        resolve_tac [TrueI]
+      end
   in
     Scan.succeed (SIMPLE_METHOD' o eval_tac)
   end
@@ -1932,7 +1935,7 @@
     SIMPLE_METHOD'
       (CHANGED_PROP o
         (CONVERSION (Nbe.dynamic_conv ctxt)
-          THEN_ALL_NEW (TRY o rtac TrueI))))
+          THEN_ALL_NEW (TRY o resolve_tac [TrueI]))))
 *} "solve goal by normalization"
 
 
@@ -1979,7 +1982,7 @@
     val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
   in
     fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
-    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
+    fun smp_tac j = EVERY'[dresolve_tac (smp j), assume_tac];
   end;
 
   local
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Product_Type.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -1324,9 +1324,10 @@
                       SOME (Goal.prove ctxt [] []
                         (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
                         (K (EVERY
-                          [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
-                           rtac subsetI 1, dtac CollectD 1, simp,
-                           rtac subsetI 1, rtac CollectI 1, simp])))
+                          [resolve_tac [eq_reflection] 1,
+                           resolve_tac @{thms subset_antisym} 1,
+                           resolve_tac [subsetI] 1, dresolve_tac [CollectD] 1, simp,
+                           resolve_tac [subsetI] 1, resolve_tac [CollectI] 1, simp])))
                     end
                   else NONE)
           | _ => NONE)
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Set.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -71,10 +71,11 @@
 simproc_setup defined_Collect ("{x. P x & Q x}") = {*
   fn _ => Quantifier1.rearrange_Collect
     (fn _ =>
-      rtac @{thm Collect_cong} 1 THEN
-      rtac @{thm iffI} 1 THEN
+      resolve_tac @{thms Collect_cong} 1 THEN
+      resolve_tac @{thms iffI} 1 THEN
       ALLGOALS
-        (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
+        (EVERY' [REPEAT_DETERM o eresolve_tac @{thms conjE},
+          DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
 *}
 
 lemmas CollectE = CollectD [elim_format]
@@ -382,7 +383,7 @@
 
 setup {*
   map_theory_claset (fn ctxt =>
-    ctxt addbefore ("bspec", fn _ => dtac @{thm bspec} THEN' assume_tac))
+    ctxt addbefore ("bspec", fn _ => dresolve_tac @{thms bspec} THEN' assume_tac))
 *}
 
 ML {*
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -113,7 +113,7 @@
             then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
             else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
      (K (rewrite_goals_tac ctxt ac
-         THEN rtac Drule.reflexive_thm 1))
+         THEN resolve_tac [Drule.reflexive_thm] 1))
  end
 
 (* instance for unions *)
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -90,7 +90,7 @@
               if Term.is_open arg then no_tac
               else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
                 THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
-                THEN_ALL_NEW etac @{thm thin_rl}
+                THEN_ALL_NEW eresolve_tac @{thms thin_rl}
                 THEN_ALL_NEW (CONVERSION
                   (params_conv ~1 (fn ctxt' =>
                     arg_conv (arg_conv (abs_conv (K conv) ctxt'))) ctxt))) i
@@ -290,7 +290,7 @@
     val rec_rule = let open Conv in
       Goal.prove lthy' (map (fst o dest_Free) args) [] eqn (fn _ =>
         CONVERSION ((arg_conv o arg1_conv o head_conv o rewr_conv) (mk_meta_eq unfold)) 1
-        THEN rtac @{thm refl} 1) end;
+        THEN resolve_tac @{thms refl} 1) end;
   in
     lthy'
     |> Local_Theory.note (eq_abinding, [rec_rule])
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -167,19 +167,19 @@
           (rename_bound_vars_RS th rl handle THM _ => tryall rls)
   in  tryall rls  end;
 
-(* Special version of "rtac" that works around an explosion in the unifier.
+(* Special version of "resolve_tac" that works around an explosion in the unifier.
    If the goal has the form "?P c", the danger is that resolving it against a
    property of the form "... c ... c ... c ..." will lead to a huge unification
    problem, due to the (spurious) choices between projection and imitation. The
    workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
-fun quant_rtac th i st =
+fun quant_resolve_tac th i st =
   case (concl_of st, prop_of th) of
     (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
     let
       val cc = cterm_of (theory_of_thm th) c
       val ct = Thm.dest_arg (cprop_of th)
-    in rtac th i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
-  | _ => rtac th i st
+    in resolve_tac [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
+  | _ => resolve_tac [th] i st
 
 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
   e.g. from conj_forward, should have the form
@@ -187,7 +187,7 @@
   and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
 fun forward_res ctxt nf st =
   let
-    fun tacf [prem] = quant_rtac (nf prem) 1
+    fun tacf [prem] = quant_resolve_tac (nf prem) 1
       | tacf prems =
         error (cat_lines
           ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
@@ -288,7 +288,7 @@
 fun forward_res2 nf hyps st =
   case Seq.pull
         (REPEAT
-         (Misc_Legacy.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
+         (Misc_Legacy.METAHYPS (fn major::minors => resolve_tac [nf (minors @ hyps) major] 1) 1)
          st)
   of SOME(th,_) => th
    | NONE => raise THM("forward_res2", 0, [st]);
@@ -700,14 +700,14 @@
 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
 
 fun skolemize_prems_tac ctxt prems =
-  cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o etac exE
+  cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o eresolve_tac [exE]
 
 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
   Function mkcl converts theorems to clauses.*)
 fun MESON preskolem_tac mkcl cltac ctxt i st =
   SELECT_GOAL
     (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
-            rtac @{thm ccontr} 1,
+            resolve_tac @{thms ccontr} 1,
             preskolem_tac,
             Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
                       EVERY1 [skolemize_prems_tac ctxt negs,
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -208,8 +208,8 @@
       |> Drule.beta_conv cabs |> Thm.apply cTrueprop
     fun tacf [prem] =
       rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
-      THEN rtac ((prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
-                 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
+      THEN resolve_tac [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
+                 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex"] 1
   in
     Goal.prove_internal ctxt [ex_tm] conc tacf
     |> forall_intr_list frees
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -531,7 +531,7 @@
     if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
   | copy_prems_tac (1 :: ms) ns i = rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
   | copy_prems_tac (m :: ms) ns i =
-    etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
+    eresolve_tac [copy_prem] i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
 
 (* Metis generates variables of the form _nnn. *)
 val is_metis_fresh_variable = String.isPrefix "_"
@@ -578,10 +578,10 @@
         end
       | _ => raise Fail "expected a single non-zapped, non-Metis Var")
   in
-    (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i) THEN PRIMITIVE do_instantiate) st
+    (DETERM (eresolve_tac @{thms allE} i THEN rotate_tac ~1 i) THEN PRIMITIVE do_instantiate) st
   end
 
-fun fix_exists_tac t = etac exE THEN' rename_tac [t |> dest_Var |> fst |> fst]
+fun fix_exists_tac t = eresolve_tac [exE] THEN' rename_tac [t |> dest_Var |> fst |> fst]
 
 fun release_quantifier_tac thy (skolem, t) =
   (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
@@ -730,7 +730,8 @@
                        cat_lines (map string_of_subst_info substs))
 *)
 
-      fun cut_and_ex_tac axiom = cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
+      fun cut_and_ex_tac axiom =
+        cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (eresolve_tac @{thms exE}) 1)
       fun rotation_of_subgoal i =
         find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
 
@@ -742,7 +743,7 @@
               THEN copy_prems_tac (map snd ax_counts) [] 1)
             THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
             THEN match_tac [prems_imp_false] 1
-            THEN ALLGOALS (fn i => rtac @{thm Meson.skolem_COMBK_I} i
+            THEN ALLGOALS (fn i => resolve_tac @{thms Meson.skolem_COMBK_I} i
               THEN rotate_tac (rotation_of_subgoal i) i
               THEN PRIMITIVE (unify_first_prem_with_concl thy i)
               THEN assume_tac i
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -61,7 +61,7 @@
 fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
   let
     val thy = Proof_Context.theory_of ctxt
-    val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN rtac refl 1
+    val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac [refl] 1
     val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
   in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end
@@ -102,7 +102,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 ctxt [] eq_ct (K (rtac eq_th 1))
+      val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (resolve_tac [eq_th] 1))
     in Thm.equal_elim eq_th' th end
 
 fun clause_params ordering =
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -150,7 +150,7 @@
           NONE => NONE
         | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u'))) (ts ~~ ts');
     val indrule' = cterm_instantiate insts indrule;
-  in rtac indrule' i end);
+  in resolve_tac [indrule'] i end);
 
 
 (* perform exhaustive case analysis on last parameter of subgoal i *)
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/Old_Datatype/old_primrec.ML
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -247,7 +247,8 @@
         val rewrites = rec_rewrites' @ map (snd o snd) defs;
       in
         map (fn eq => Goal.prove ctxt frees [] eq
-          (fn {context = ctxt', ...} => EVERY [rewrite_goals_tac ctxt' rewrites, rtac refl 1])) eqs
+          (fn {context = ctxt', ...} =>
+            EVERY [rewrite_goals_tac ctxt' rewrites, resolve_tac [refl] 1])) eqs
       end;
   in ((prefix, (fs, defs)), prove) end
   handle PrimrecError (msg, some_eqn) =>
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -57,10 +57,10 @@
           (Logic.strip_imp_concl t)
           (fn {prems, ...} =>
             EVERY
-              [rtac induct' 1,
-               REPEAT (rtac TrueI 1),
-               REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
-               REPEAT (rtac TrueI 1)])
+              [resolve_tac [induct'] 1,
+               REPEAT (resolve_tac [TrueI] 1),
+               REPEAT ((resolve_tac [impI] 1) THEN (eresolve_tac prems 1)),
+               REPEAT (resolve_tac [TrueI] 1)])
       end;
 
     val casedist_thms =
@@ -176,16 +176,16 @@
           in
             (EVERY
               [DETERM tac,
-                REPEAT (etac @{thm ex1E} 1), rtac @{thm ex1I} 1,
+                REPEAT (eresolve_tac @{thms ex1E} 1), resolve_tac @{thms ex1I} 1,
                 DEPTH_SOLVE_1 (ares_tac [intr] 1),
-                REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
-                etac elim 1,
+                REPEAT_DETERM_N k (eresolve_tac [thin_rl] 1 THEN rotate_tac 1 1),
+                eresolve_tac [elim] 1,
                 REPEAT_DETERM_N j distinct_tac,
                 TRY (dresolve_tac inject 1),
-                REPEAT (etac conjE 1), hyp_subst_tac ctxt 1,
-                REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
+                REPEAT (eresolve_tac [conjE] 1), hyp_subst_tac ctxt 1,
+                REPEAT (EVERY [eresolve_tac [allE] 1, dresolve_tac [mp] 1, assume_tac 1]),
                 TRY (hyp_subst_tac ctxt 1),
-                rtac refl 1,
+                resolve_tac [refl] 1,
                 REPEAT_DETERM_N (n - j - 1) distinct_tac],
               intrs, j + 1)
           end;
@@ -211,7 +211,7 @@
           (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj rec_unique_ts))
           (fn {context = ctxt, ...} =>
             #1 (fold (mk_unique_tac ctxt) (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
-              (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
+              (((resolve_tac [induct'] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
                   rewrite_goals_tac ctxt [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
       end;
 
@@ -254,10 +254,10 @@
         Goal.prove_sorry_global thy2 [] [] t
           (fn {context = ctxt, ...} => EVERY
             [rewrite_goals_tac ctxt reccomb_defs,
-             rtac @{thm the1_equality} 1,
+             resolve_tac @{thms the1_equality} 1,
              resolve_tac rec_unique_thms 1,
              resolve_tac rec_intrs 1,
-             REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
+             REPEAT (resolve_tac [allI] 1 ORELSE resolve_tac rec_total_thms 1)]))
        (Old_Datatype_Prop.make_primrecs reccomb_names descr thy2);
   in
     thy2
@@ -338,7 +338,8 @@
 
     fun prove_case t =
       Goal.prove_sorry_global thy2 [] [] t (fn {context = ctxt, ...} =>
-        EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]);
+        EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms),
+          resolve_tac [refl] 1]);
 
     fun prove_cases (Type (Tcon, _)) ts =
       (case Ctr_Sugar.ctr_sugar_of ctxt Tcon of
@@ -379,7 +380,7 @@
         val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion)));
         val exhaustion' = cterm_instantiate [(cert lhs, cert (Free ("x", T)))] exhaustion;
         fun tac ctxt =
-          EVERY [rtac exhaustion' 1,
+          EVERY [resolve_tac [exhaustion'] 1,
             ALLGOALS (asm_simp_tac
               (put_simpset HOL_ss ctxt addsimps (dist_rewrites' @ inject @ case_thms')))];
       in
@@ -405,7 +406,7 @@
   let
     fun prove_case_cong_weak t =
      Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
-       (fn {prems, ...} => EVERY [rtac (hd prems RS arg_cong) 1]);
+       (fn {prems, ...} => EVERY [resolve_tac [hd prems RS arg_cong] 1]);
 
     val case_cong_weaks =
       map prove_case_cong_weak (Old_Datatype_Prop.make_case_cong_weaks case_names descr thy);
@@ -423,12 +424,13 @@
       let
         (* For goal i, select the correct disjunct to attack, then prove it *)
         fun tac ctxt i 0 =
-              EVERY [TRY (rtac disjI1 i), hyp_subst_tac ctxt i, REPEAT (rtac exI i), rtac refl i]
-          | tac ctxt i n = rtac disjI2 i THEN tac ctxt i (n - 1);
+              EVERY [TRY (resolve_tac [disjI1] i), hyp_subst_tac ctxt i,
+                REPEAT (resolve_tac [exI] i), resolve_tac [refl] i]
+          | tac ctxt i n = resolve_tac [disjI2] i THEN tac ctxt i (n - 1);
       in
         Goal.prove_sorry_global thy [] [] t
           (fn {context = ctxt, ...} =>
-            EVERY [rtac allI 1,
+            EVERY [resolve_tac [allI] 1,
              Old_Datatype_Aux.exh_tac (K exhaustion) 1,
              ALLGOALS (fn i => tac ctxt i (i - 1))])
       end;
@@ -457,8 +459,8 @@
               EVERY [
                 simp_tac (put_simpset HOL_ss ctxt addsimps [hd prems]) 1,
                 cut_tac nchotomy'' 1,
-                REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
-                REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
+                REPEAT (eresolve_tac [disjE] 1 THEN REPEAT (eresolve_tac [exE] 1) THEN simplify 1),
+                REPEAT (eresolve_tac [exE] 1) THEN simplify 1 (* Get last disjunct *)]
             end)
       end;
 
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/cnf.ML
--- a/src/HOL/Tools/cnf.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/cnf.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -141,7 +141,7 @@
       if i > nprems_of thm then
         thm
       else
-        not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm))
+        not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (resolve_tac [clause2raw_not_disj] i) thm))
     (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
     (* becomes "[..., A1, ..., An] |- B"                                   *)
     (* Thm.thm -> Thm.thm *)
@@ -154,7 +154,7 @@
     (* [...] |- ~x1 ==> ... ==> ~xn ==> False *)
     |> not_disj_to_prem 1
     (* [...] |- x1' ==> ... ==> xn' ==> False *)
-    |> Seq.hd o TRYALL (rtac clause2raw_not_not)
+    |> Seq.hd o TRYALL (resolve_tac [clause2raw_not_not])
     (* [..., x1', ..., xn'] |- False *)
     |> prems_to_hyps
   end;
@@ -529,7 +529,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun weakening_tac i =
-  dtac weakening_thm i THEN atac (i+1);
+  dresolve_tac [weakening_thm] i THEN assume_tac (i+1);
 
 (* ------------------------------------------------------------------------- *)
 (* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/coinduction.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -37,7 +37,7 @@
   let
     val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
   in
-    (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
+    (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve_tac [thin_rl])) i st
   end;
 
 fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
@@ -87,13 +87,15 @@
           val e = length eqs;
           val p = length prems;
         in
-          HEADGOAL (EVERY' [rtac thm,
+          HEADGOAL (EVERY' [resolve_tac [thm],
             EVERY' (map (fn var =>
-              rtac (cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI)) vars),
-            if p = 0 then CONJ_WRAP' (K (rtac refl)) eqs
-            else REPEAT_DETERM_N e o (rtac conjI THEN' rtac refl) THEN' CONJ_WRAP' rtac prems,
+              resolve_tac [cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI]) vars),
+            if p = 0 then CONJ_WRAP' (K (resolve_tac [refl])) eqs
+            else
+              REPEAT_DETERM_N e o (resolve_tac [conjI] THEN' resolve_tac [refl]) THEN'
+              CONJ_WRAP' (resolve_tac o single) prems,
             K (ALLGOALS_SKIP skip
-               (REPEAT_DETERM_N (length vars) o (etac exE THEN' rotate_tac ~1) THEN'
+               (REPEAT_DETERM_N (length vars) o (eresolve_tac [exE] THEN' rotate_tac ~1) THEN'
                DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
                  (case prems of
                    [] => all_tac
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -169,8 +169,8 @@
   | mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n);
 
 fun select_disj 1 1 = []
-  | select_disj _ 1 = [rtac disjI1]
-  | select_disj n i = rtac disjI2 :: select_disj (n - 1) (i - 1);
+  | select_disj _ 1 = [resolve_tac [disjI1]]
+  | select_disj n i = resolve_tac [disjI2] :: select_disj (n - 1) (i - 1);
 
 
 
@@ -378,12 +378,13 @@
     [] []
     (HOLogic.mk_Trueprop
       (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
-    (fn _ => EVERY [rtac @{thm monoI} 1,
+    (fn _ => EVERY [resolve_tac @{thms monoI} 1,
       REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
       REPEAT (FIRST
-        [atac 1,
+        [assume_tac 1,
          resolve_tac (map (mk_mono ctxt) monos @ get_monos ctxt) 1,
-         etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
+         eresolve_tac @{thms le_funE} 1,
+         dresolve_tac @{thms le_boolD} 1])]));
 
 
 (* prove introduction rules *)
@@ -401,7 +402,7 @@
     val intrs = map_index (fn (i, intr) =>
       Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY
        [rewrite_goals_tac ctxt rec_preds_defs,
-        rtac (unfold RS iffD2) 1,
+        resolve_tac [unfold RS iffD2] 1,
         EVERY1 (select_disj (length intr_ts) (i + 1)),
         (*Not ares_tac, since refl must be tried before any equality assumptions;
           backtracking may occur if the premises have extra variables!*)
@@ -447,7 +448,7 @@
           (fn {context = ctxt4, prems} => EVERY
             [cut_tac (hd prems) 1,
              rewrite_goals_tac ctxt4 rec_preds_defs,
-             dtac (unfold RS iffD1) 1,
+             dresolve_tac [unfold RS iffD1] 1,
              REPEAT (FIRSTGOAL (eresolve_tac rules1)),
              REPEAT (FIRSTGOAL (eresolve_tac rules2)),
              EVERY (map (fn prem =>
@@ -494,37 +495,39 @@
         val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
         fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
             EVERY1 (select_disj (length c_intrs) (i + 1)) THEN
-            EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN
-            (if null prems then rtac @{thm TrueI} 1
+            EVERY (replicate (length params) (resolve_tac @{thms exI} 1)) THEN
+            (if null prems then resolve_tac @{thms TrueI} 1
              else
               let
                 val (prems', last_prem) = split_last prems;
               in
-                EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN
-                rtac last_prem 1
+                EVERY (map (fn prem =>
+                  (resolve_tac @{thms conjI} 1 THEN resolve_tac [prem] 1)) prems') THEN
+                resolve_tac [last_prem] 1
               end)) ctxt' 1;
         fun prove_intr2 (((_, _, us, _), ts, params'), intr) =
-          EVERY (replicate (length params') (etac @{thm exE} 1)) THEN
-          (if null ts andalso null us then rtac intr 1
+          EVERY (replicate (length params') (eresolve_tac @{thms exE} 1)) THEN
+          (if null ts andalso null us then resolve_tac [intr] 1
            else
-            EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
+            EVERY (replicate (length ts + length us - 1) (eresolve_tac @{thms conjE} 1)) THEN
             Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} =>
               let
                 val (eqs, prems') = chop (length us) prems;
                 val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
               in
                 rewrite_goal_tac ctxt'' rew_thms 1 THEN
-                rtac intr 1 THEN
-                EVERY (map (fn p => rtac p 1) prems')
+                resolve_tac [intr] 1 THEN
+                EVERY (map (fn p => resolve_tac [p] 1) prems')
               end) ctxt' 1);
       in
         Goal.prove_sorry ctxt' [] [] eq (fn _ =>
-          rtac @{thm iffI} 1 THEN etac (#1 elim) 1 THEN
+          resolve_tac @{thms iffI} 1 THEN
+          eresolve_tac [#1 elim] 1 THEN
           EVERY (map_index prove_intr1 c_intrs) THEN
-          (if null c_intrs then etac @{thm FalseE} 1
+          (if null c_intrs then eresolve_tac @{thms FalseE} 1
            else
             let val (c_intrs', last_c_intr) = split_last c_intrs in
-              EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs') THEN
+              EVERY (map (fn ci => eresolve_tac @{thms disjE} 1 THEN prove_intr2 ci) c_intrs') THEN
               prove_intr2 last_c_intr
             end))
         |> rulify ctxt'
@@ -729,16 +732,16 @@
     val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl
       (fn {context = ctxt3, prems} => EVERY
         [rewrite_goals_tac ctxt3 [inductive_conj_def],
-         DETERM (rtac raw_fp_induct 1),
+         DETERM (resolve_tac [raw_fp_induct] 1),
          REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
          rewrite_goals_tac ctxt3 simp_thms2,
          (*This disjE separates out the introduction rules*)
          REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
          (*Now break down the individual cases.  No disjE here in case
            some premise involves disjunction.*)
-         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt3)),
+         REPEAT (FIRSTGOAL (eresolve_tac [conjE] ORELSE' bound_hyp_subst_tac ctxt3)),
          REPEAT (FIRSTGOAL
-           (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
+           (resolve_tac [conjI, impI] ORELSE' (eresolve_tac [notE] THEN' assume_tac))),
          EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3
              (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
            conjI, refl] 1)) prems)]);
@@ -749,9 +752,9 @@
          REPEAT (EVERY
            [REPEAT (resolve_tac [conjI, impI] 1),
             REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
-            atac 1,
+            assume_tac 1,
             rewrite_goals_tac ctxt3 simp_thms1,
-            atac 1])]);
+            assume_tac 1])]);
 
   in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
 
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -75,11 +75,14 @@
               SOME (close (Goal.prove ctxt [] [])
                 (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S'))))
                 (K (EVERY
-                  [rtac eq_reflection 1, REPEAT (rtac @{thm ext} 1), rtac iffI 1,
-                   EVERY [etac conjE 1, rtac IntI 1, simp, simp,
-                     etac IntE 1, rtac conjI 1, simp, simp] ORELSE
-                   EVERY [etac disjE 1, rtac UnI1 1, simp, rtac UnI2 1, simp,
-                     etac UnE 1, rtac disjI1 1, simp, rtac disjI2 1, simp]])))
+                  [resolve_tac [eq_reflection] 1, REPEAT (resolve_tac @{thms ext} 1),
+                   resolve_tac [iffI] 1,
+                   EVERY [eresolve_tac [conjE] 1, resolve_tac [IntI] 1, simp, simp,
+                     eresolve_tac [IntE] 1, resolve_tac [conjI] 1, simp, simp] ORELSE
+                   EVERY [eresolve_tac [disjE] 1, resolve_tac [UnI1] 1, simp,
+                     resolve_tac [UnI2] 1, simp,
+                     eresolve_tac [UnE] 1, resolve_tac [disjI1] 1, simp,
+                     resolve_tac [disjI2] 1, simp]])))
                 handle ERROR _ => NONE))
     in
       case strip_comb t of
@@ -502,8 +505,9 @@
                fold_rev (Term.abs o pair "x") Ts
                 (HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
                   list_comb (c, params))))))
-            (K (REPEAT (rtac @{thm ext} 1) THEN simp_tac (put_simpset HOL_basic_ss lthy addsimps
-              [def, mem_Collect_eq, @{thm split_conv}]) 1))
+            (K (REPEAT (resolve_tac @{thms ext} 1) THEN
+              simp_tac (put_simpset HOL_basic_ss lthy addsimps
+                [def, mem_Collect_eq, @{thm split_conv}]) 1))
         in
           lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
             [Attrib.internal (K pred_set_conv_att)]),
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -731,11 +731,11 @@
       end)
   in
     EVERY' [
-      REPEAT_DETERM o etac rev_mp,
+      REPEAT_DETERM o eresolve_tac [rev_mp],
       cond_split_tac,
-      rtac @{thm ccontr},
+      resolve_tac @{thms ccontr},
       prem_nnf_tac ctxt,
-      TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
+      TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' eresolve_tac [disjE]))
     ]
   end;
 
@@ -758,7 +758,7 @@
             THEN_ALL_NEW
               (CONVERSION Drule.beta_eta_conversion
                 THEN'
-              (TRY o (etac notE THEN' eq_assume_tac)))
+              (TRY o (eresolve_tac [notE] THEN' eq_assume_tac)))
         ) i
     )
   end;
@@ -835,11 +835,12 @@
         REPEAT_DETERM
               (eresolve_tac [@{thm conjE}, @{thm exE}] 1 ORELSE
                filter_prems_tac test 1 ORELSE
-               etac @{thm disjE} 1) THEN
-        (DETERM (etac @{thm notE} 1 THEN eq_assume_tac 1) ORELSE
+               eresolve_tac @{thms disjE} 1) THEN
+        (DETERM (eresolve_tac @{thms notE} 1 THEN eq_assume_tac 1) ORELSE
          ref_tac 1);
   in EVERY'[TRY o filter_prems_tac test,
-            REPEAT_DETERM o etac @{thm rev_mp}, prep_tac, rtac @{thm ccontr}, prem_nnf_tac ctxt,
+            REPEAT_DETERM o eresolve_tac @{thms rev_mp}, prep_tac,
+              resolve_tac @{thms ccontr}, prem_nnf_tac ctxt,
             SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   end;
 
@@ -872,7 +873,8 @@
 
 fun gen_tac ex ctxt =
   FIRST' [simple_tac ctxt,
-    Object_Logic.full_atomize_tac ctxt THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
+    Object_Logic.full_atomize_tac ctxt THEN'
+    (REPEAT_DETERM o resolve_tac [impI]) THEN' raw_tac ctxt ex];
 
 val tac = gen_tac true;
 
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/sat.ML
--- a/src/HOL/Tools/sat.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/sat.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -406,7 +406,7 @@
 
 fun rawsat_tac ctxt i =
   Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
-    rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
+    resolve_tac [rawsat_thm ctxt' (map cprop_of prems)] 1) ctxt i;
 
 (* ------------------------------------------------------------------------- *)
 (* pre_cnf_tac: converts the i-th subgoal                                    *)
@@ -421,7 +421,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun pre_cnf_tac ctxt =
-  rtac @{thm ccontr} THEN'
+  resolve_tac @{thms ccontr} THEN'
   Object_Logic.atomize_prems_tac ctxt THEN'
   CONVERSION Drule.beta_eta_conversion;
 
@@ -433,7 +433,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun cnfsat_tac ctxt i =
-  (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
+  (eresolve_tac [FalseE] i) ORELSE (REPEAT_DETERM (eresolve_tac [conjE] i) THEN rawsat_tac ctxt i);
 
 (* ------------------------------------------------------------------------- *)
 (* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
@@ -443,8 +443,8 @@
 (* ------------------------------------------------------------------------- *)
 
 fun cnfxsat_tac ctxt i =
-  (etac FalseE i) ORELSE
-    (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
+  (eresolve_tac [FalseE] i) ORELSE
+    (REPEAT_DETERM (eresolve_tac [conjE] i ORELSE eresolve_tac [exE] i) THEN rawsat_tac ctxt i);
 
 (* ------------------------------------------------------------------------- *)
 (* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -314,95 +314,96 @@
 val collectI' = @{lemma "\<not> P a ==> a \<notin> {x. P x}" by auto}
 val collectE' = @{lemma "a \<notin> {x. P x} ==> (\<not> P a ==> Q) ==> Q" by auto}
 
-fun elim_Collect_tac ctxt = dtac @{thm iffD1[OF mem_Collect_eq]}
+fun elim_Collect_tac ctxt = dresolve_tac @{thms iffD1 [OF mem_Collect_eq]}
   THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
-  THEN' REPEAT_DETERM o etac @{thm conjE}
+  THEN' REPEAT_DETERM o eresolve_tac @{thms conjE}
   THEN' TRY o hyp_subst_tac ctxt;
 
-fun intro_image_tac ctxt = rtac @{thm image_eqI}
+fun intro_image_tac ctxt = resolve_tac @{thms image_eqI}
     THEN' (REPEAT_DETERM1 o
-      (rtac @{thm refl}
-      ORELSE' rtac
-        @{thm arg_cong2[OF refl, where f="op =", OF prod.case, THEN iffD2]}
+      (resolve_tac @{thms refl}
+      ORELSE' resolve_tac @{thms arg_cong2 [OF refl, where f = "op =", OF prod.case, THEN iffD2]}
       ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
         (HOLogic.Trueprop_conv
           (HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_distrib)))))) ctxt)))
 
-fun elim_image_tac ctxt = etac @{thm imageE}
+fun elim_image_tac ctxt = eresolve_tac @{thms imageE}
   THEN' REPEAT_DETERM o CHANGED o
     (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
-    THEN' REPEAT_DETERM o etac @{thm Pair_inject}
+    THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
     THEN' TRY o hyp_subst_tac ctxt)
 
 fun tac1_of_formula ctxt (Int (fm1, fm2)) =
-    TRY o etac @{thm conjE}
-    THEN' rtac @{thm IntI}
+    TRY o eresolve_tac @{thms conjE}
+    THEN' resolve_tac @{thms IntI}
     THEN' (fn i => tac1_of_formula ctxt fm2 (i + 1))
     THEN' tac1_of_formula ctxt fm1
   | tac1_of_formula ctxt (Un (fm1, fm2)) =
-    etac @{thm disjE} THEN' rtac @{thm UnI1}
+    eresolve_tac @{thms disjE} THEN' resolve_tac @{thms UnI1}
     THEN' tac1_of_formula ctxt fm1
-    THEN' rtac @{thm UnI2}
+    THEN' resolve_tac @{thms UnI2}
     THEN' tac1_of_formula ctxt fm2
   | tac1_of_formula ctxt (Atom _) =
-    REPEAT_DETERM1 o (atac
-      ORELSE' rtac @{thm SigmaI}
-      ORELSE' ((rtac @{thm CollectI} ORELSE' rtac collectI') THEN'
+    REPEAT_DETERM1 o (assume_tac
+      ORELSE' resolve_tac @{thms SigmaI}
+      ORELSE' ((resolve_tac @{thms CollectI} ORELSE' resolve_tac [collectI']) THEN'
         TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
-      ORELSE' ((rtac @{thm vimageI2} ORELSE' rtac vimageI2') THEN'
+      ORELSE' ((resolve_tac @{thms vimageI2} ORELSE' resolve_tac [vimageI2']) THEN'
         TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
-      ORELSE' (rtac @{thm image_eqI} THEN'
+      ORELSE' (resolve_tac @{thms image_eqI} THEN'
     (REPEAT_DETERM o
-      (rtac @{thm refl}
-      ORELSE' rtac @{thm arg_cong2[OF refl, where f="op =", OF prod.case, THEN iffD2]})))
-      ORELSE' rtac @{thm UNIV_I}
-      ORELSE' rtac @{thm iffD2[OF Compl_iff]}
-      ORELSE' atac)
+      (resolve_tac @{thms refl}
+      ORELSE' resolve_tac @{thms arg_cong2[OF refl, where f = "op =", OF prod.case, THEN iffD2]})))
+      ORELSE' resolve_tac @{thms UNIV_I}
+      ORELSE' resolve_tac @{thms iffD2[OF Compl_iff]}
+      ORELSE' assume_tac)
 
 fun tac2_of_formula ctxt (Int (fm1, fm2)) =
-    TRY o etac @{thm IntE}
-    THEN' TRY o rtac @{thm conjI}
+    TRY o eresolve_tac @{thms IntE}
+    THEN' TRY o resolve_tac @{thms conjI}
     THEN' (fn i => tac2_of_formula ctxt fm2 (i + 1))
     THEN' tac2_of_formula ctxt fm1
   | tac2_of_formula ctxt (Un (fm1, fm2)) =
-    etac @{thm UnE} THEN' rtac @{thm disjI1}
+    eresolve_tac @{thms UnE} THEN' resolve_tac @{thms disjI1}
     THEN' tac2_of_formula ctxt fm1
-    THEN' rtac @{thm disjI2}
+    THEN' resolve_tac @{thms disjI2}
     THEN' tac2_of_formula ctxt fm2
   | tac2_of_formula ctxt (Atom _) =
     REPEAT_DETERM o
-      (atac
-       ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]}
-       ORELSE' etac @{thm conjE}
-       ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN'
+      (assume_tac
+       ORELSE' dresolve_tac @{thms iffD1[OF mem_Sigma_iff]}
+       ORELSE' eresolve_tac @{thms conjE}
+       ORELSE' ((eresolve_tac @{thms CollectE} ORELSE' eresolve_tac [collectE']) THEN'
          TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]) THEN'
-         REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})
-       ORELSE' (etac @{thm imageE}
+         REPEAT_DETERM o eresolve_tac @{thms Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN'
+         TRY o resolve_tac @{thms refl})
+       ORELSE' (eresolve_tac @{thms imageE}
          THEN' (REPEAT_DETERM o CHANGED o
          (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
-         THEN' REPEAT_DETERM o etac @{thm Pair_inject}
-         THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})))
-       ORELSE' etac @{thm ComplE}
-       ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE')
+         THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
+         THEN' TRY o hyp_subst_tac ctxt THEN' TRY o resolve_tac @{thms refl})))
+       ORELSE' eresolve_tac @{thms ComplE}
+       ORELSE' ((eresolve_tac @{thms vimageE} ORELSE' eresolve_tac [vimageE'])
         THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}])
-        THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl}))
+        THEN' TRY o hyp_subst_tac ctxt THEN' TRY o resolve_tac @{thms refl}))
 
 fun tac ctxt fm =
   let
-    val subset_tac1 = rtac @{thm subsetI}
+    val subset_tac1 = resolve_tac @{thms subsetI}
       THEN' elim_Collect_tac ctxt
       THEN' intro_image_tac ctxt
       THEN' tac1_of_formula ctxt fm
-    val subset_tac2 = rtac @{thm subsetI}
+    val subset_tac2 = resolve_tac @{thms subsetI}
       THEN' elim_image_tac ctxt
-      THEN' rtac @{thm iffD2[OF mem_Collect_eq]}
+      THEN' resolve_tac @{thms iffD2[OF mem_Collect_eq]}
       THEN' REPEAT_DETERM o resolve_tac @{thms exI}
-      THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
-      THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac ctxt) THEN' rtac @{thm refl}))))
+      THEN' (TRY o REPEAT_ALL_NEW (resolve_tac @{thms conjI}))
+      THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac ctxt) THEN' resolve_tac @{thms refl}))))
       THEN' (fn i => EVERY (rev (map_index (fn (j, f) =>
-        REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula ctxt f (i + j)) (strip_Int fm))))
+        REPEAT_DETERM (eresolve_tac @{thms IntE} (i + j)) THEN
+        tac2_of_formula ctxt f (i + j)) (strip_Int fm))))
   in
-    rtac @{thm subset_antisym} THEN' subset_tac1 THEN' subset_tac2
+    resolve_tac @{thms subset_antisym} THEN' subset_tac1 THEN' subset_tac2
   end;
 
 
@@ -429,18 +430,18 @@
     fun is_eq th = is_some (try (HOLogic.dest_eq o HOLogic.dest_Trueprop) (prop_of th))
     val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.case}
     fun tac ctxt = 
-      rtac @{thm set_eqI}
+      resolve_tac @{thms set_eqI}
       THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps unfold_thms)
-      THEN' rtac @{thm iffI}
-      THEN' REPEAT_DETERM o rtac @{thm exI}
-      THEN' rtac @{thm conjI} THEN' rtac @{thm refl} THEN' atac
-      THEN' REPEAT_DETERM o etac @{thm exE}
-      THEN' etac @{thm conjE}
-      THEN' REPEAT_DETERM o etac @{thm Pair_inject}
+      THEN' resolve_tac @{thms iffI}
+      THEN' REPEAT_DETERM o resolve_tac @{thms exI}
+      THEN' resolve_tac @{thms conjI} THEN' resolve_tac @{thms refl} THEN' assume_tac
+      THEN' REPEAT_DETERM o eresolve_tac @{thms exE}
+      THEN' eresolve_tac @{thms conjE}
+      THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
       THEN' Subgoal.FOCUS (fn {prems, ...} =>
         (* FIXME inner context!? *)
         simp_tac (put_simpset HOL_basic_ss ctxt addsimps (filter is_eq prems)) 1) ctxt
-      THEN' TRY o atac
+      THEN' TRY o assume_tac
   in
     case try mk_term (term_of ct) of
       NONE => Thm.reflexive ct
diff -r 773b378d9313 -r f4bb3068d819 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -81,7 +81,7 @@
 (*Congruence rules for = (instead of ==)*)
 fun mk_meta_cong (_: Proof.context) rl = zero_var_indexes
   (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
-     rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
+     resolve_tac [lift_meta_eq_to_obj_eq i st] i st) rl)
    in mk_meta_eq rl' handle THM _ =>
      if can Logic.dest_equals (concl_of rl') then rl'
      else error "Conclusion of congruence rules must be =-equality"
@@ -119,7 +119,7 @@
     val sol_thms =
       reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
     fun sol_tac i =
-      FIRST [resolve_tac sol_thms i, atac i , etac @{thm FalseE} i] ORELSE
+      FIRST [resolve_tac sol_thms i, assume_tac i , eresolve_tac @{thms FalseE} i] ORELSE
       (match_tac intros THEN_ALL_NEW sol_tac) i
   in
     (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' sol_tac
diff -r 773b378d9313 -r f4bb3068d819 src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Provers/Arith/cancel_numerals.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -92,12 +92,12 @@
     Option.map (export o Data.simplify_meta_eq ctxt)
       (if n2 <= n1 then
          Data.prove_conv
-           [Data.trans_tac reshape, rtac Data.bal_add1 1,
+           [Data.trans_tac reshape, resolve_tac [Data.bal_add1] 1,
             Data.numeral_simp_tac ctxt] ctxt prems
            (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
        else
          Data.prove_conv
-           [Data.trans_tac reshape, rtac Data.bal_add2 1,
+           [Data.trans_tac reshape, resolve_tac [Data.bal_add2] 1,
             Data.numeral_simp_tac ctxt] ctxt prems
            (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
   end
diff -r 773b378d9313 -r f4bb3068d819 src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Provers/Arith/combine_numerals.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -83,7 +83,7 @@
   in
     Option.map (export o Data.simplify_meta_eq ctxt)
       (Data.prove_conv
-         [Data.trans_tac reshape, rtac Data.left_distrib 1,
+         [Data.trans_tac reshape, resolve_tac [Data.left_distrib] 1,
           Data.numeral_simp_tac ctxt] ctxt
          (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
   end
diff -r 773b378d9313 -r f4bb3068d819 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -815,7 +815,7 @@
           all_tac) THEN
           PRIMITIVE (trace_thm ctxt ["State after neqE:"]) THEN
           (* use theorems generated from the actual justifications *)
-          Subgoal.FOCUS (fn {prems, ...} => rtac (mkthm ctxt prems j) 1) ctxt i
+          Subgoal.FOCUS (fn {prems, ...} => resolve_tac [mkthm ctxt prems j] 1) ctxt i
     in
       (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
       DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
diff -r 773b378d9313 -r f4bb3068d819 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Provers/blast.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -488,8 +488,8 @@
 
 (*Resolution/matching tactics: if upd then the proof state may be updated.
   Matching makes the tactics more deterministic in the presence of Vars.*)
-fun emtac ctxt upd rl = TRACE ctxt rl (if upd then etac rl else ematch_tac [rl]);
-fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then rtac rl else match_tac [rl]);
+fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac [rl]);
+fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac [rl]);
 
 (*Tableau rule from elimination rule.
   Flag "upd" says that the inference updated the branch.
@@ -624,7 +624,7 @@
 
 (*Tactic.  Convert *Goal* to negated assumption in FIRST position*)
 fun negOfGoal_tac ctxt i =
-  TRACE ctxt Data.ccontr (rtac Data.ccontr) i THEN rotate_tac ~1 i;
+  TRACE ctxt Data.ccontr (resolve_tac [Data.ccontr]) i THEN rotate_tac ~1 i;
 
 fun traceTerm ctxt t =
   let val thy = Proof_Context.theory_of ctxt
diff -r 773b378d9313 -r f4bb3068d819 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Provers/classical.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -157,7 +157,7 @@
       val rule'' =
         rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
           if i = 1 orelse redundant_hyp goal
-          then etac thin_rl i
+          then eresolve_tac [thin_rl] i
           else all_tac))
         |> Seq.hd
         |> Drule.zero_var_indexes;
@@ -209,7 +209,7 @@
   let
     val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
     val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
-  in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
+  in rule_by_tactic ctxt (TRYALL (eresolve_tac [revcut_rl])) rl end;
 
 
 (**** Classical rule sets ****)
@@ -689,8 +689,8 @@
 fun ctxt addafter (name, tac2) =
   ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt);
 
-fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dtac thm THEN' assume_tac);
-fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => etac thm THEN' assume_tac);
+fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
+fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
 fun ctxt addSD2 (name, thm) = ctxt addSafter (name, fn _ => dmatch_tac [thm] THEN' eq_assume_tac);
 fun ctxt addSE2 (name, thm) = ctxt addSafter (name, fn _ => ematch_tac [thm] THEN' eq_assume_tac);
 
@@ -909,7 +909,7 @@
     val ruleq = Drule.multi_resolves facts rules;
     val _ = Method.trace ctxt rules;
   in
-    fn st => Seq.maps (fn rule => rtac rule i st) ruleq
+    fn st => Seq.maps (fn rule => resolve_tac [rule] i st) ruleq
   end)
   THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
 
diff -r 773b378d9313 -r f4bb3068d819 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Provers/hypsubst.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -126,7 +126,7 @@
      val (k, _) = eq_var false false false t
      val ok = (eq_var false false true t |> fst) > k
         handle EQ_VAR => true
-   in if ok then EVERY [rotate_tac k i, etac thin_rl i, rotate_tac (~k) i]
+   in if ok then EVERY [rotate_tac k i, eresolve_tac [thin_rl] i, rotate_tac (~k) i]
     else no_tac
    end handle EQ_VAR => no_tac)
 
@@ -151,11 +151,11 @@
         val (k, (orient, is_free)) = eq_var bnd true true Bi
         val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
-        if not is_free then etac thin_rl i
-          else if orient then etac Data.rev_mp i
-          else etac (Data.sym RS Data.rev_mp) i,
+        if not is_free then eresolve_tac [thin_rl] i
+          else if orient then eresolve_tac [Data.rev_mp] i
+          else eresolve_tac [Data.sym RS Data.rev_mp] i,
         rotate_tac (~k) i,
-        if is_free then rtac Data.imp_intr i else all_tac]
+        if is_free then resolve_tac [Data.imp_intr] i else all_tac]
       end handle THM _ => no_tac | EQ_VAR => no_tac)
 
 end;
@@ -194,7 +194,7 @@
       end
   | NONE => no_tac);
 
-val imp_intr_tac = rtac Data.imp_intr;
+val imp_intr_tac = resolve_tac [Data.imp_intr];
 
 fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
 val dup_subst = rev_dup_elim ssubst
@@ -211,9 +211,9 @@
           val rl = if orient then rl else Data.sym RS rl
       in
          DETERM
-           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
+           (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
                    rotate_tac 1 i,
-                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
+                   REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
                    inst_subst_tac orient rl i,
                    REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
       end
@@ -245,7 +245,7 @@
 fun reverse_n_tac 0 i = all_tac
   | reverse_n_tac 1 i = rotate_tac ~1 i
   | reverse_n_tac n i =
-      REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
+      REPEAT_DETERM_N n (rotate_tac ~1 i THEN eresolve_tac [Data.rev_mp] i) THEN
       REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
 
 (*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
@@ -279,9 +279,9 @@
       in
          if trace then tracing "Substituting an equality" else ();
          DETERM
-           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
+           (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
                    rotate_tac 1 i,
-                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
+                   REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
                    inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
                    all_imp_intr_tac hyps i])
       end
@@ -291,7 +291,7 @@
   fails unless the substitution has an effect*)
 fun stac th =
   let val th' = th RS Data.rev_eq_reflection handle THM _ => th
-  in CHANGED_GOAL (rtac (th' RS ssubst)) end;
+  in CHANGED_GOAL (resolve_tac [th' RS ssubst]) end;
 
 
 (* method setup *)
diff -r 773b378d9313 -r f4bb3068d819 src/Provers/order.ML
--- a/src/Provers/order.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Provers/order.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -1243,10 +1243,10 @@
   in
    Subgoal.FOCUS (fn {prems = asms, ...} =>
      let val thms = map (prove (prems @ asms)) prfs
-     in rtac (prove thms prf) 1 end) ctxt n st
+     in resolve_tac [prove thms prf] 1 end) ctxt n st
   end
   handle Contr p =>
-      (Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
+      (Subgoal.FOCUS (fn {prems = asms, ...} => resolve_tac [prove asms p] 1) ctxt n st
         handle General.Subscript => Seq.empty)
    | Cannot => Seq.empty
    | General.Subscript => Seq.empty)
diff -r 773b378d9313 -r f4bb3068d819 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Provers/quantifier1.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -126,10 +126,10 @@
       yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
     val thm =
       Goal.prove ctxt' [] [] goal
-        (fn {context = ctxt'', ...} => rtac Data.iff_reflection 1 THEN tac ctxt'');
+        (fn {context = ctxt'', ...} => resolve_tac [Data.iff_reflection] 1 THEN tac ctxt'');
   in singleton (Variable.export ctxt' ctxt) thm end;
 
-fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i);
+fun qcomm_tac qcomm qI i = REPEAT_DETERM (resolve_tac [qcomm] i THEN resolve_tac [qI] i);
 
 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
    Better: instantiate exI
@@ -138,9 +138,10 @@
   val excomm = Data.ex_comm RS Data.iff_trans;
 in
   val prove_one_point_ex_tac =
-    qcomm_tac excomm Data.iff_exI 1 THEN rtac Data.iffI 1 THEN
+    qcomm_tac excomm Data.iff_exI 1 THEN resolve_tac [Data.iffI] 1 THEN
     ALLGOALS
-      (EVERY' [etac Data.exE, REPEAT_DETERM o etac Data.conjE, rtac Data.exI,
+      (EVERY' [eresolve_tac [Data.exE], REPEAT_DETERM o eresolve_tac [Data.conjE],
+        resolve_tac [Data.exI],
         DEPTH_SOLVE_1 o ares_tac [Data.conjI]])
 end;
 
@@ -150,12 +151,17 @@
 local
   val tac =
     SELECT_GOAL
-      (EVERY1 [REPEAT o dtac Data.uncurry, REPEAT o rtac Data.impI, etac Data.mp,
-        REPEAT o etac Data.conjE, REPEAT o ares_tac [Data.conjI]]);
+      (EVERY1 [REPEAT o dresolve_tac [Data.uncurry],
+        REPEAT o resolve_tac [Data.impI],
+        eresolve_tac [Data.mp],
+        REPEAT o eresolve_tac [Data.conjE],
+        REPEAT o ares_tac [Data.conjI]]);
   val allcomm = Data.all_comm RS Data.iff_trans;
 in
   val prove_one_point_all_tac =
-    EVERY1 [qcomm_tac allcomm Data.iff_allI, rtac Data.iff_allI, rtac Data.iffI, tac, tac];
+    EVERY1 [qcomm_tac allcomm Data.iff_allI,
+      resolve_tac [Data.iff_allI],
+      resolve_tac [Data.iffI], tac, tac];
 end
 
 fun renumber l u (Bound i) =
diff -r 773b378d9313 -r f4bb3068d819 src/Provers/quasi.ML
--- a/src/Provers/quasi.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Provers/quasi.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -565,9 +565,9 @@
  in
   Subgoal.FOCUS (fn {prems, ...} =>
     let val thms = map (prove prems) prfs
-    in rtac (prove thms prf) 1 end) ctxt n st
+    in resolve_tac [prove thms prf] 1 end) ctxt n st
  end
- handle Contr p => Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
+ handle Contr p => Subgoal.FOCUS (fn {prems, ...} => resolve_tac [prove prems p] 1) ctxt n st
   | Cannot  => Seq.empty);
 
 
@@ -585,10 +585,10 @@
  in
   Subgoal.FOCUS (fn {prems, ...} =>
     let val thms = map (prove prems) prfs
-    in rtac (prove thms prf) 1 end) ctxt n st
+    in resolve_tac [prove thms prf] 1 end) ctxt n st
  end
  handle Contr p =>
-    (Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
+    (Subgoal.FOCUS (fn {prems, ...} => resolve_tac [prove prems p] 1) ctxt n st
       handle General.Subscript => Seq.empty)
   | Cannot => Seq.empty
   | General.Subscript => Seq.empty);
diff -r 773b378d9313 -r f4bb3068d819 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Provers/splitter.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -99,7 +99,7 @@
 val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
   [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
   (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
-  (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN rtac reflexive_thm 1)
+  (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN resolve_tac [reflexive_thm] 1)
 
 val _ $ _ $ (_ $ (_ $ abs_lift) $ _) = prop_of lift;
 
@@ -365,11 +365,11 @@
                    (case apsns of
                       [] => compose_tac (false, inst_split Ts t tt thm TB state i, 0) i state
                     | p::_ => EVERY [lift_tac Ts t p,
-                                     rtac reflexive_thm (i+1),
+                                     resolve_tac [reflexive_thm] (i+1),
                                      lift_split_tac] state)
             end
   in COND (has_fewer_prems i) no_tac
-          (rtac meta_iffD i THEN lift_split_tac)
+          (resolve_tac [meta_iffD] i THEN lift_split_tac)
   end;
 
 in (split_tac, exported_split_posns) end;  (* mk_case_split_tac *)
@@ -400,16 +400,16 @@
       (* does not work properly if the split variable is bound by a quantifier *)
               fun flat_prems_tac i = SUBGOAL (fn (t,i) =>
                            (if first_prem_is_disj t
-                            then EVERY[etac Data.disjE i,rotate_tac ~1 i,
+                            then EVERY[eresolve_tac [Data.disjE] i, rotate_tac ~1 i,
                                        rotate_tac ~1  (i+1),
                                        flat_prems_tac (i+1)]
                             else all_tac)
                            THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i)
                            THEN REPEAT (dresolve_tac [Data.notnotD]   i)) i;
           in if n<0 then  no_tac  else (DETERM (EVERY'
-                [rotate_tac n, etac Data.contrapos2,
+                [rotate_tac n, eresolve_tac [Data.contrapos2],
                  split_tac splits,
-                 rotate_tac ~1, etac Data.contrapos, rotate_tac ~1,
+                 rotate_tac ~1, eresolve_tac [Data.contrapos], rotate_tac ~1,
                  flat_prems_tac] i))
           end;
   in SUBGOAL tac
diff -r 773b378d9313 -r f4bb3068d819 src/Provers/trancl.ML
--- a/src/Provers/trancl.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Provers/trancl.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -545,7 +545,7 @@
     let
       val SOME (_, _, rel', _) = decomp (term_of concl);
       val thms = map (prove thy rel' prems) prfs
-    in rtac (prove thy rel' thms prf) 1 end) ctxt n st
+    in resolve_tac [prove thy rel' thms prf] 1 end) ctxt n st
  end
  handle Cannot => Seq.empty);
 
@@ -564,7 +564,7 @@
     let
       val SOME (_, _, rel', _) = decomp (term_of concl);
       val thms = map (prove thy rel' prems) prfs
-    in rtac (prove thy rel' thms prf) 1 end) ctxt n st
+    in resolve_tac [prove thy rel' thms prf] 1 end) ctxt n st
  end
  handle Cannot => Seq.empty | General.Subscript => Seq.empty);
 
diff -r 773b378d9313 -r f4bb3068d819 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Pure/Isar/class.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -434,7 +434,7 @@
         (fst o rules thy) sub];
     val classrel =
       Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
-        (K (EVERY (map (TRYALL o rtac) intros)));
+        (K (EVERY (map (TRYALL o resolve_tac o single) intros)));
     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub])
       |> filter (is_class thy);
diff -r 773b378d9313 -r f4bb3068d819 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -56,7 +56,7 @@
         val loc_intro_tac =
           (case Locale.intros_of thy class of
             (_, NONE) => all_tac
-          | (_, SOME intro) => ALLGOALS (rtac intro));
+          | (_, SOME intro) => ALLGOALS (resolve_tac [intro]));
         val tac = loc_intro_tac
           THEN ALLGOALS (Proof_Context.fact_tac empty_ctxt (sup_axioms @ the_list assm_axiom));
       in Element.prove_witness empty_ctxt prop tac end) some_prop;
diff -r 773b378d9313 -r f4bb3068d819 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Pure/Isar/element.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -258,14 +258,15 @@
 fun prove_witness ctxt t tac =
   Witness (t,
     Thm.close_derivation
-      (Goal.prove ctxt [] [] (mark_witness t) (fn _ => rtac Drule.protectI 1 THEN tac)));
+      (Goal.prove ctxt [] [] (mark_witness t)
+        (fn _ => resolve_tac [Drule.protectI] 1 THEN tac)));
 
 
 local
 
 val refine_witness =
   Proof.refine (Method.Basic (K (NO_CASES o
-    K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI)))))))));
+    K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (resolve_tac [Drule.protectI])))))))));
 
 fun gen_witness_proof proof after_qed wit_propss eq_props =
   let
diff -r 773b378d9313 -r f4bb3068d819 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Pure/Isar/method.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -100,7 +100,7 @@
 local
 
 fun cut_rule_tac rule =
-  rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
+  resolve_tac [Drule.forall_intr_vars rule COMP_INCR revcut_rl];
 
 in
 
@@ -147,7 +147,7 @@
 
 (* this -- resolve facts directly *)
 
-val this = METHOD (EVERY o map (HEADGOAL o rtac));
+val this = METHOD (EVERY o map (HEADGOAL o resolve_tac o single));
 
 
 (* fact -- composition by facts from context *)
@@ -162,7 +162,7 @@
 
 fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
   if cond (Logic.strip_assums_concl prop)
-  then rtac rule i else no_tac);
+  then resolve_tac [rule] i else no_tac);
 
 in
 
diff -r 773b378d9313 -r f4bb3068d819 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -442,12 +442,12 @@
       Goal.norm_hhf_tac ctxt THEN'
       SUBGOAL (fn (goal, i) =>
         if can Logic.unprotect (Logic.strip_assums_concl goal) then
-          etac Drule.protectI i THEN finish_tac ctxt (n - 1) i
+          eresolve_tac [Drule.protectI] i THEN finish_tac ctxt (n - 1) i
         else finish_tac ctxt (n - 1) (i + 1));
 
 fun goal_tac ctxt rule =
   Goal.norm_hhf_tac ctxt THEN'
-  rtac rule THEN'
+  resolve_tac [rule] THEN'
   finish_tac ctxt (Thm.nprems_of rule);
 
 fun FINDGOAL tac st =
@@ -886,7 +886,7 @@
 fun refine_terms n =
   refine (Method.Basic (K (NO_CASES o
     K (HEADGOAL (PRECISE_CONJUNCTS n
-      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))))
+      (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac [Drule.termI])))))))))
   #> Seq.hd;
 
 in
diff -r 773b378d9313 -r f4bb3068d819 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -206,9 +206,10 @@
     val goal' = Thm.transfer thy' goal;
 
     fun limited_etac thm i =
-      Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o etac thm i;
+      Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o
+        eresolve_tac [thm] i;
     fun try_thm thm =
-      if Thm.no_prems thm then rtac thm 1 goal'
+      if Thm.no_prems thm then resolve_tac [thm] 1 goal'
       else
         (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
           1 goal';
diff -r 773b378d9313 -r f4bb3068d819 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Pure/goal.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -293,7 +293,7 @@
 
 val adhoc_conjunction_tac = REPEAT_ALL_NEW
   (SUBGOAL (fn (goal, i) =>
-    if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
+    if can Logic.dest_conjunction goal then resolve_tac [Conjunction.conjunctionI] i
     else no_tac));
 
 val conjunction_tac = SUBGOAL (fn (goal, i) =>
@@ -317,7 +317,7 @@
 (* hhf normal form *)
 
 fun norm_hhf_tac ctxt =
-  rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
+  resolve_tac [Drule.asm_rl]  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   THEN' SUBGOAL (fn (t, i) =>
     if Drule.is_norm_hhf t then all_tac
     else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i);
@@ -335,7 +335,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 =>
-      etac (Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)) THEN_ALL_NEW assume_tac);
+      eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac);
   in fold_rev (curry op APPEND') tacs (K no_tac) i end);
 
 end;
diff -r 773b378d9313 -r f4bb3068d819 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Pure/raw_simplifier.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -148,7 +148,7 @@
  {thm: thm,         (*the rewrite rule*)
   name: string,     (*name of theorem from which rewrite rule was extracted*)
   lhs: term,        (*the left-hand side*)
-  elhs: cterm,      (*the etac-contracted lhs*)
+  elhs: cterm,      (*the eta-contracted lhs*)
   extra: bool,      (*extra variables outside of elhs*)
   fo: bool,         (*use first-order matching*)
   perm: bool};      (*the rewrite rule is permutative*)
diff -r 773b378d9313 -r f4bb3068d819 src/Pure/skip_proof.ML
--- a/src/Pure/skip_proof.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Pure/skip_proof.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -38,6 +38,6 @@
 (* cheat_tac *)
 
 fun cheat_tac i st =
-  rtac (make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))) i st;
+  resolve_tac [make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))] i st;
 
 end;
diff -r 773b378d9313 -r f4bb3068d819 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Pure/tactic.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -181,7 +181,7 @@
 
 (*The conclusion of the rule gets assumed in subgoal i,
   while subgoal i+1,... are the premises of the rule.*)
-fun cut_tac rule i = rtac cut_rl i THEN rtac rule (i + 1);
+fun cut_tac rule i = resolve_tac [cut_rl] i THEN resolve_tac [rule] (i + 1);
 
 (*"Cut" a list of rules into the goal.  Their premises will become new
   subgoals.*)
@@ -327,7 +327,7 @@
         | Then (SOME tac) tac' = SOME(tac THEN' tac');
       fun thins H (tac,n) =
         if p H then (tac,n+1)
-        else (Then tac (rotate_tac n THEN' etac thin_rl),0);
+        else (Then tac (rotate_tac n THEN' eresolve_tac [thin_rl]),0);
   in SUBGOAL(fn (subg,n) =>
        let val Hs = Logic.strip_assums_hyp subg
        in case fst(fold thins Hs (NONE,0)) of
diff -r 773b378d9313 -r f4bb3068d819 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Pure/thm.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -1390,7 +1390,7 @@
 
 (*Rotates a rule's premises to the left by k, leaving the first j premises
   unchanged.  Does nothing if k=0 or if k equals n-j, where n is the
-  number of premises.  Useful with etac and underlies defer_tac*)
+  number of premises.  Useful with eresolve_tac and underlies defer_tac*)
 fun permute_prems j k rl =
   let
     val Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...}) = rl;
diff -r 773b378d9313 -r f4bb3068d819 src/Tools/case_product.ML
--- a/src/Tools/case_product.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Tools/case_product.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -70,9 +70,9 @@
     val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
     val thm2' = thm2 OF p_cons2
   in
-    rtac (thm1 OF p_cons1)
+    resolve_tac [thm1 OF p_cons1]
      THEN' EVERY' (map (fn p =>
-       rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
+       resolve_tac [thm2'] THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
   end
 
 fun combine ctxt thm1 thm2 =
diff -r 773b378d9313 -r f4bb3068d819 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Tools/coherent.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -215,7 +215,7 @@
 (** external interface **)
 
 fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
-  rtac (rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2) 1 THEN
+  resolve_tac [rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2] 1 THEN
   SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
     let
       val xs =
@@ -227,7 +227,7 @@
         valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
           (mk_dom xs) Net.empty 0 0 of
         NONE => no_tac
-      | SOME prf => rtac (thm_of_cl_prf ctxt'' concl [] prf) 1)
+      | SOME prf => resolve_tac [thm_of_cl_prf ctxt'' concl [] prf] 1)
     end) ctxt' 1) ctxt;
 
 val _ = Theory.setup
diff -r 773b378d9313 -r f4bb3068d819 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Tools/eqsubst.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -250,7 +250,7 @@
   RW_Inst.rw ctxt m rule conclthm
   |> unfix_frees cfvs
   |> Conv.fconv_rule Drule.beta_eta_conversion
-  |> (fn r => rtac r i st);
+  |> (fn r => resolve_tac [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 *)
@@ -332,7 +332,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)) (dtac preelimrule i st2)
+    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dresolve_tac [preelimrule] i st2)
   end;
 
 
diff -r 773b378d9313 -r f4bb3068d819 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Tools/induct.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -512,7 +512,7 @@
         in
           CASES (Rule_Cases.make_common (thy,
               Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
-            ((Method.insert_tac more_facts THEN' rtac rule' THEN_ALL_NEW
+            ((Method.insert_tac more_facts THEN' resolve_tac [rule'] THEN_ALL_NEW
                 (if simp then TRY o trivial_tac else K all_tac)) i) st
         end)
   end;
@@ -683,7 +683,8 @@
   in
     (case goal_concl n [] goal of
       SOME concl =>
-        (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i
+        (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN'
+          resolve_tac [asm_rl]) i
     | NONE => all_tac)
   end);
 
@@ -804,7 +805,7 @@
               |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
               |> Seq.maps (fn rule' =>
                 CASES (rule_cases ctxt rule' cases)
-                  (rtac rule' i THEN
+                  (resolve_tac [rule'] i THEN
                     PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
       end)
       THEN_ALL_NEW_CASES
@@ -862,7 +863,7 @@
         |> Seq.maps (fn rule' =>
           CASES (Rule_Cases.make_common (thy,
               Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
-            (Method.insert_tac more_facts i THEN rtac rule' i) st))
+            (Method.insert_tac more_facts i THEN resolve_tac [rule'] i) st))
   end);
 
 end;
diff -r 773b378d9313 -r f4bb3068d819 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Oct 30 23:14:11 2014 +0100
@@ -230,7 +230,7 @@
     key_pressed = (evt: KeyEvent) =>
       {
         evt.getKeyCode match {
-          case KeyEvent.VK_C
+          case KeyEvent.VK_C | KeyEvent.VK_INSERT
           if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 &&
               text_area.getSelectionCount != 0 =>
             Registers.copy(text_area, '$')
diff -r 773b378d9313 -r f4bb3068d819 src/ZF/Datatype_ZF.thy
--- a/src/ZF/Datatype_ZF.thy	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/ZF/Datatype_ZF.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -95,7 +95,7 @@
          else ();
        val goal = Logic.mk_equals (old, new)
        val thm = Goal.prove ctxt [] [] goal
-         (fn _ => rtac @{thm iff_reflection} 1 THEN
+         (fn _ => resolve_tac @{thms iff_reflection} 1 THEN
            simp_tac (put_simpset datatype_ss ctxt addsimps #free_iffs lcon_info) 1)
          handle ERROR msg =>
          (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal);
diff -r 773b378d9313 -r f4bb3068d819 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -289,7 +289,7 @@
       (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
       (fn {context = ctxt, ...} => EVERY
         [rewrite_goals_tac ctxt [con_def],
-         rtac case_trans 1,
+         resolve_tac [case_trans] 1,
          REPEAT
            (resolve_tac [@{thm refl}, split_trans,
              Su.case_inl RS @{thm trans}, Su.case_inr RS @{thm trans}] 1)]);
@@ -330,7 +330,7 @@
             (Ind_Syntax.traceIt "next recursor equation = " thy1 (mk_recursor_eqn arg))
             (*Proves a single recursor equation.*)
             (fn {context = ctxt, ...} => EVERY
-              [rtac recursor_trans 1,
+              [resolve_tac [recursor_trans] 1,
                simp_tac (put_simpset rank_ss ctxt addsimps case_eqns) 1,
                IF_UNSOLVED (simp_tac (put_simpset rank_ss ctxt addsimps tl con_defs) 1)]);
       in
diff -r 773b378d9313 -r f4bb3068d819 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -189,7 +189,7 @@
   val bnd_mono =
     Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
       (fn _ => EVERY
-        [rtac (@{thm Collect_subset} RS @{thm bnd_monoI}) 1,
+        [resolve_tac [@{thm Collect_subset} RS @{thm bnd_monoI}] 1,
          REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]);
 
   val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs);
@@ -218,13 +218,13 @@
     [DETERM (stac unfold 1),
      REPEAT (resolve_tac [@{thm Part_eqI}, @{thm CollectI}] 1),
      (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
-     rtac disjIn 2,
+     resolve_tac [disjIn] 2,
      (*Not ares_tac, since refl must be tried before equality assumptions;
        backtracking may occur if the premises have extra variables!*)
      DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2),
      (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
      rewrite_goals_tac ctxt con_defs,
-     REPEAT (rtac @{thm refl} 2),
+     REPEAT (resolve_tac @{thms refl} 2),
      (*Typechecking; this can fail*)
      if !Ind_Syntax.trace then print_tac ctxt "The type-checking subgoal:"
      else all_tac,
@@ -332,15 +332,15 @@
            setSolver (mk_solver "minimal"
                       (fn ctxt => resolve_tac (triv_rls @ Simplifier.prems_of ctxt)
                                    ORELSE' assume_tac
-                                   ORELSE' etac @{thm FalseE}));
+                                   ORELSE' eresolve_tac @{thms FalseE}));
 
      val quant_induct =
        Goal.prove_global thy1 [] ind_prems
          (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
          (fn {context = ctxt, prems} => EVERY
            [rewrite_goals_tac ctxt part_rec_defs,
-            rtac (@{thm impI} RS @{thm allI}) 1,
-            DETERM (etac raw_induct 1),
+            resolve_tac [@{thm impI} RS @{thm allI}] 1,
+            DETERM (eresolve_tac [raw_induct] 1),
             (*Push Part inside Collect*)
             full_simp_tac (min_ss addsimps [@{thm Part_Collect}]) 1,
             (*This CollectE and disjE separates out the introduction rules*)
@@ -470,8 +470,8 @@
                       (mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1
                    THEN
                    (*unpackage and use "prem" in the corresponding place*)
-                   REPEAT (rtac @{thm impI} 1)  THEN
-                   rtac (rewrite_rule ctxt all_defs prem) 1  THEN
+                   REPEAT (resolve_tac @{thms impI} 1)  THEN
+                   resolve_tac [rewrite_rule ctxt all_defs prem] 1  THEN
                    (*prem must not be REPEATed below: could loop!*)
                    DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
                                            eresolve_tac (@{thm conjE} :: @{thm mp} :: cmonos))))
@@ -483,7 +483,7 @@
          Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
            mutual_induct_concl
            (fn {context = ctxt, prems} => EVERY
-             [rtac (quant_induct RS lemma) 1,
+             [resolve_tac [quant_induct RS lemma] 1,
               mutual_ind_tac ctxt (rev prems) (length prems)])
        else @{thm TrueI};
 
diff -r 773b378d9313 -r f4bb3068d819 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -176,7 +176,8 @@
     val eqn_thms =
       eqn_terms |> map (fn t =>
         Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
-          (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac @{thm refl} 1]));
+          (fn {context = ctxt, ...} =>
+            EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac @{thms refl} 1]));
 
     val (eqn_thms', thy2) =
       thy1
diff -r 773b378d9313 -r f4bb3068d819 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/ZF/Tools/typechk.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -99,7 +99,7 @@
 (*Instantiates variables in typing conditions.
   drawback: does not simplify conjunctions*)
 fun type_solver_tac ctxt hyps = SELECT_GOAL
-    (DEPTH_SOLVE (etac @{thm FalseE} 1
+    (DEPTH_SOLVE (eresolve_tac @{thms FalseE} 1
                   ORELSE basic_res_tac 1
                   ORELSE (ares_tac hyps 1
                           APPEND typecheck_step_tac (tcset_of ctxt))));
diff -r 773b378d9313 -r f4bb3068d819 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Thu Oct 30 21:02:01 2014 +0100
+++ b/src/ZF/arith_data.ML	Thu Oct 30 23:14:11 2014 +0100
@@ -51,7 +51,7 @@
 
 (*Apply the given rewrite (if present) just once*)
 fun gen_trans_tac th2 NONE      = all_tac
-  | gen_trans_tac th2 (SOME th) = ALLGOALS (rtac (th RS th2));
+  | gen_trans_tac th2 (SOME th) = ALLGOALS (resolve_tac [th RS th2]);
 
 (*Use <-> or = depending on the type of t*)
 fun mk_eq_iff(t,u) =