# HG changeset patch
# User wenzelm
# Date 1423583181 -3600
# Node ID 14095f771781b59006ba160b41a31802617d8d8b
# Parent  50b60f501b05367f6838a1d97dc4ff4ec9537377
misc tuning;

diff -r 50b60f501b05 -r 14095f771781 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/CCL/CCL.thy	Tue Feb 10 16:46:21 2015 +0100
@@ -204,7 +204,8 @@
       fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
       val inj_lemmas = maps mk_inj_lemmas rews
     in
-      CHANGED (REPEAT (ares_tac [@{thm iffI}, @{thm allI}, @{thm conjI}] i ORELSE
+      CHANGED (REPEAT (assume_tac ctxt i ORELSE
+        resolve_tac ctxt @{thms iffI allI conjI} i ORELSE
         eresolve_tac ctxt inj_lemmas i ORELSE
         asm_simp_tac (ctxt addsimps rews) i))
     end;
diff -r 50b60f501b05 -r 14095f771781 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/CCL/Type.thy	Tue Feb 10 16:46:21 2015 +0100
@@ -127,9 +127,10 @@
 fun mk_ncanT_tac top_crls crls =
   SUBPROOF (fn {context = ctxt, prems = major :: prems, ...} =>
     resolve_tac ctxt ([major] RL top_crls) 1 THEN
-    REPEAT_SOME (eresolve_tac ctxt (crls @ [@{thm exE}, @{thm bexE}, @{thm conjE}, @{thm disjE}])) THEN
+    REPEAT_SOME (eresolve_tac ctxt (crls @ @{thms exE bexE conjE disjE})) THEN
     ALLGOALS (asm_simp_tac ctxt) THEN
-    ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN
+    ALLGOALS (assume_tac ctxt ORELSE' resolve_tac ctxt (prems RL [@{thm lem}])
+      ORELSE' eresolve_tac ctxt @{thms bspec}) THEN
     safe_tac (ctxt addSIs prems))
 *}
 
diff -r 50b60f501b05 -r 14095f771781 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/CCL/Wfd.thy	Tue Feb 10 16:46:21 2015 +0100
@@ -451,10 +451,11 @@
   THEN eresolve_tac ctxt @{thms rcall_lemmas} i
 
 fun raw_step_tac ctxt prems i =
-  ares_tac (prems@type_rls) i ORELSE
+  assume_tac ctxt i ORELSE
+  resolve_tac ctxt (prems @ type_rls) i ORELSE
   rcall_tac ctxt i ORELSE
-  ematch_tac ctxt [@{thm SubtypeE}] i ORELSE
-  match_tac ctxt [@{thm SubtypeI}] i
+  ematch_tac ctxt @{thms SubtypeE} i ORELSE
+  match_tac ctxt @{thms SubtypeI} i
 
 fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
     if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
diff -r 50b60f501b05 -r 14095f771781 src/Cube/Example.thy
--- a/src/Cube/Example.thy	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/Cube/Example.thy	Tue Feb 10 16:46:21 2015 +0100
@@ -10,17 +10,17 @@
   J. Functional Programming.\<close>
 
 method_setup depth_solve =
-  \<open>Attrib.thms >> (fn thms => K (METHOD (fn facts =>
-    (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))\<close>
+  \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
+    (DEPTH_SOLVE (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close>
 
 method_setup depth_solve1 =
-  \<open>Attrib.thms >> (fn thms => K (METHOD (fn facts =>
-    (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))\<close>
+  \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
+    (DEPTH_SOLVE_1 (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close>
 
 method_setup strip_asms =
   \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
     REPEAT (resolve_tac ctxt [@{thm strip_b}, @{thm strip_s}] 1 THEN
-    DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))\<close>
+    DEPTH_SOLVE_1 (assume_tac ctxt 1 ORELSE resolve_tac ctxt (facts @ thms) 1))))\<close>
 
 
 subsection \<open>Simple types\<close>
diff -r 50b60f501b05 -r 14095f771781 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/HOL.thy	Tue Feb 10 16:46:21 2015 +0100
@@ -904,7 +904,8 @@
   shows R
 apply (rule ex1E [OF major])
 apply (rule prem)
-apply (tactic {* ares_tac @{thms allI} 1 *})+
+apply assumption
+apply (rule allI)+
 apply (tactic {* eresolve_tac @{context} [Classical.dup_elim NONE @{thm allE}] 1 *})
 apply iprover
 done
diff -r 50b60f501b05 -r 14095f771781 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Feb 10 16:46:21 2015 +0100
@@ -1061,7 +1061,8 @@
          EVERY (map (fn (prem, r) => (EVERY
            [REPEAT (eresolve_tac ctxt Abs_inverse_thms' 1),
             simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
-            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
+            DEPTH_SOLVE_1
+              (assume_tac ctxt 1 ORELSE resolve_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
                 (prems ~~ constr_defs))]);
 
     val case_names_induct = Old_Datatype_Data.mk_case_names_induct descr'';
diff -r 50b60f501b05 -r 14095f771781 src/HOL/SET_Protocol/Cardholder_Registration.thy
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Tue Feb 10 16:46:21 2015 +0100
@@ -538,7 +538,7 @@
 method_setup valid_certificate_tac = {*
   Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant
     (fn i =>
-      EVERY [ftac @{thm Gets_certificate_valid} i,
+      EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i,
              assume_tac ctxt i,
              etac conjE i, REPEAT (hyp_subst_tac ctxt i)]))
 *}
diff -r 50b60f501b05 -r 14095f771781 src/HOL/SET_Protocol/Purchase.thy
--- a/src/HOL/SET_Protocol/Purchase.thy	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/SET_Protocol/Purchase.thy	Tue Feb 10 16:46:21 2015 +0100
@@ -482,7 +482,7 @@
 method_setup valid_certificate_tac = {*
   Args.goal_spec >> (fn quant =>
     fn ctxt => SIMPLE_METHOD'' quant (fn i =>
-      EVERY [ftac @{thm Gets_certificate_valid} i,
+      EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i,
              assume_tac ctxt i, REPEAT (hyp_subst_tac ctxt i)]))
 *}
 
diff -r 50b60f501b05 -r 14095f771781 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/Set.thy	Tue Feb 10 16:46:21 2015 +0100
@@ -75,7 +75,7 @@
       resolve_tac ctxt @{thms iffI} 1 THEN
       ALLGOALS
         (EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms conjE},
-          DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
+          DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})]))
 *}
 
 lemmas CollectE = CollectD [elim_format]
diff -r 50b60f501b05 -r 14095f771781 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Feb 10 16:46:21 2015 +0100
@@ -94,7 +94,7 @@
    REPEAT_DETERM o (rtac (subset_UNIV RS conjI) ORELSE' etac conjI), atac] 1;
 
 fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
-  (EVERY' [rtac notI, hyp_subst_tac ctxt, ftac alg_set] THEN'
+  (EVERY' [rtac notI, hyp_subst_tac ctxt, forward_tac ctxt [alg_set]] THEN'
   REPEAT_DETERM o FIRST'
     [EVERY' [rtac @{thm subset_emptyI}, eresolve_tac ctxt wits],
     EVERY' [rtac subsetI, rtac FalseE, eresolve_tac ctxt wits],
diff -r 50b60f501b05 -r 14095f771781 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Feb 10 16:46:21 2015 +0100
@@ -452,7 +452,8 @@
              REPEAT (FIRSTGOAL (eresolve_tac ctxt4 rules1)),
              REPEAT (FIRSTGOAL (eresolve_tac ctxt4 rules2)),
              EVERY (map (fn prem =>
-               DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1))
+               DEPTH_SOLVE_1 (assume_tac ctxt4 1 ORELSE
+                resolve_tac ctxt [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1))
                 (tl prems))])
           |> singleton (Proof_Context.export ctxt'' ctxt'''),
          map #2 c_intrs, length Ts)
@@ -746,9 +747,11 @@
          REPEAT (FIRSTGOAL
            (resolve_tac ctxt3 [conjI, impI] ORELSE'
            (eresolve_tac ctxt3 [notE] THEN' assume_tac ctxt3))),
-         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)]);
+         EVERY (map (fn prem =>
+            DEPTH_SOLVE_1 (assume_tac ctxt3 1 ORELSE
+              resolve_tac ctxt3
+                [rewrite_rule ctxt3 (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
+                  conjI, refl] 1)) prems)]);
 
     val lemma = Goal.prove_sorry ctxt'' [] []
       (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn {context = ctxt3, ...} => EVERY
diff -r 50b60f501b05 -r 14095f771781 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/Tools/simpdata.ML	Tue Feb 10 16:46:21 2015 +0100
@@ -73,8 +73,10 @@
           (mk_simp_implies @{prop "(x::'a) = y"})
           (fn {context = ctxt, prems} => EVERY
            [rewrite_goals_tac ctxt @{thms simp_implies_def},
-            REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
-              map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)])
+            REPEAT (assume_tac ctxt 1 ORELSE
+              resolve_tac ctxt
+                (@{thm meta_eq_to_obj_eq} ::
+                  map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)])
       end
   end;