# HG changeset patch
# User wenzelm
# Date 1414682446 -3600
# Node ID e84d900cd287a0f914199ae36af3b3676621d57b
# Parent  4037bb00d08e06d07843958f6761c2fa033da0bd
eliminated aliases;

diff -r 4037bb00d08e -r e84d900cd287 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/Isar/class.ML	Thu Oct 30 16:20:46 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 4037bb00d08e -r e84d900cd287 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Thu Oct 30 16:20:46 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 4037bb00d08e -r e84d900cd287 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/Isar/element.ML	Thu Oct 30 16:20:46 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 4037bb00d08e -r e84d900cd287 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/Isar/method.ML	Thu Oct 30 16:20:46 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 4037bb00d08e -r e84d900cd287 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Oct 30 16:20:46 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 4037bb00d08e -r e84d900cd287 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Thu Oct 30 16:20:46 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 4037bb00d08e -r e84d900cd287 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/goal.ML	Thu Oct 30 16:20:46 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 4037bb00d08e -r e84d900cd287 src/Pure/skip_proof.ML
--- a/src/Pure/skip_proof.ML	Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/skip_proof.ML	Thu Oct 30 16:20:46 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 4037bb00d08e -r e84d900cd287 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/tactic.ML	Thu Oct 30 16:20:46 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 4037bb00d08e -r e84d900cd287 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Oct 30 16:17:56 2014 +0100
+++ b/src/Pure/thm.ML	Thu Oct 30 16:20:46 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;