# HG changeset patch
# User wenzelm
# Date 1437248658 -7200
# Node ID c09598a974360ae95464c997bada49a8706c2abe
# Parent  f122140b7195a00908ebec540c1ef3e7aea59d39
prefer tactics with explicit context;

diff -r f122140b7195 -r c09598a97436 src/HOL/Library/bnf_lfp_countable.ML
--- a/src/HOL/Library/bnf_lfp_countable.ML	Sat Jul 18 21:25:55 2015 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML	Sat Jul 18 21:44:18 2015 +0200
@@ -24,8 +24,8 @@
 val countableS = @{sort countable};
 
 fun nchotomy_tac ctxt nchotomy =
-  HEADGOAL (rtac ctxt (nchotomy RS @{thm all_reg[rotated]}) THEN'
-    REPEAT_ALL_NEW (resolve0_tac [allI, impI] ORELSE' eresolve0_tac [exE, disjE]));
+  HEADGOAL (resolve_tac ctxt [nchotomy RS @{thm all_reg[rotated]}] THEN'
+    REPEAT_ALL_NEW (resolve_tac ctxt [allI, impI] ORELSE' eresolve_tac ctxt [exE, disjE]));
 
 fun meta_spec_mp_tac ctxt 0 = K all_tac
   | meta_spec_mp_tac ctxt depth =
diff -r f122140b7195 -r c09598a97436 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sat Jul 18 21:25:55 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sat Jul 18 21:44:18 2015 +0200
@@ -247,7 +247,7 @@
           val ordIso = Const (@{const_name ordIso}, HOLogic.mk_setT (fastype_of bd_bd'));
           val goal = mk_Trueprop_mem (bd_bd', ordIso);
         in
-          (bd', SOME (Goal.prove_sorry lthy [] [] goal (K bd_ordIso_natLeq_tac)
+          (bd', SOME (Goal.prove_sorry lthy [] [] goal (bd_ordIso_natLeq_tac o #context)
             |> Thm.close_derivation))
         end
       else
diff -r f122140b7195 -r c09598a97436 src/HOL/Tools/BNF/bnf_comp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Sat Jul 18 21:25:55 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Sat Jul 18 21:44:18 2015 +0200
@@ -32,7 +32,7 @@
   val mk_simple_rel_OO_Grp_tac: Proof.context -> thm -> thm -> tactic
   val mk_simple_wit_tac: Proof.context -> thm list -> tactic
   val mk_simplified_set_tac: Proof.context -> thm -> tactic
-  val bd_ordIso_natLeq_tac: tactic
+  val bd_ordIso_natLeq_tac: Proof.context -> tactic
 end;
 
 structure BNF_Comp_Tactics : BNF_COMP_TACTICS =
@@ -233,7 +233,7 @@
   rtac ctxt (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
 
 fun mk_simple_wit_tac ctxt wit_thms =
-  ALLGOALS (assume_tac ctxt ORELSE' eresolve0_tac (@{thm emptyE} :: wit_thms));
+  ALLGOALS (assume_tac ctxt ORELSE' eresolve_tac ctxt (@{thm emptyE} :: wit_thms));
 
 val csum_thms =
   @{thms csum_cong1 csum_cong2 csum_cong  csum_dup[OF natLeq_cinfinite natLeq_Card_order]};
@@ -248,8 +248,8 @@
   unfold_thms_tac ctxt (collect_set_map :: @{thms comp_assoc}) THEN
   unfold_thms_tac ctxt simplified_set_simps THEN rtac ctxt refl 1;
 
-val bd_ordIso_natLeq_tac =
-  HEADGOAL (REPEAT_DETERM o resolve0_tac
+fun bd_ordIso_natLeq_tac ctxt =
+  HEADGOAL (REPEAT_DETERM o resolve_tac ctxt
     (@{thm ordIso_refl[OF natLeq_Card_order]} :: csum_thms @ cprod_thms));
 
 end;
diff -r f122140b7195 -r c09598a97436 src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sat Jul 18 21:25:55 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sat Jul 18 21:44:18 2015 +0200
@@ -55,13 +55,15 @@
   (hyp_subst_tac ctxt THEN' rtac ctxt cong0 THEN'
    REPEAT_DETERM o (dtac ctxt meta_spec THEN' etac ctxt meta_mp THEN' assume_tac ctxt)) 1;
 fun mk_set_map set_map0 = set_map0 RS @{thm comp_eq_dest};
-fun mk_in_mono_tac ctxt n = if n = 0 then rtac ctxt subset_UNIV 1
-  else (rtac ctxt subsetI THEN'
-  rtac ctxt CollectI) 1 THEN
-  REPEAT_DETERM (eresolve0_tac [CollectE, conjE] 1) THEN
-  REPEAT_DETERM_N (n - 1)
-    ((rtac ctxt conjI THEN' etac ctxt subset_trans THEN' assume_tac ctxt) 1) THEN
-  (etac ctxt subset_trans THEN' assume_tac ctxt) 1;
+
+fun mk_in_mono_tac ctxt n =
+  if n = 0 then rtac ctxt subset_UNIV 1
+  else
+   (rtac ctxt subsetI THEN' rtac ctxt CollectI) 1 THEN
+   REPEAT_DETERM (eresolve_tac ctxt [CollectE, conjE] 1) THEN
+   REPEAT_DETERM_N (n - 1)
+     ((rtac ctxt conjI THEN' etac ctxt subset_trans THEN' assume_tac ctxt) 1) THEN
+   (etac ctxt subset_trans THEN' assume_tac ctxt) 1;
 
 fun mk_inj_map_tac ctxt n map_id map_comp map_cong0 map_cong =
   let
diff -r f122140b7195 -r c09598a97436 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sat Jul 18 21:25:55 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sat Jul 18 21:44:18 2015 +0200
@@ -128,7 +128,7 @@
       HEADGOAL (rtac ctxt (rotate_prems ~1 exhaust_disc) THEN' assume_tac ctxt THEN'
       REPEAT_DETERM o (rotate_tac ~1 THEN' dtac ctxt (rotate_prems 1 iffD) THEN'
         assume_tac ctxt THEN' rotate_tac ~1 THEN'
-        etac ctxt (rotate_prems 1 notE) THEN' eresolve0_tac distinct_disc));
+        etac ctxt (rotate_prems 1 notE) THEN' eresolve_tac ctxt distinct_disc));
   in
     HEADGOAL Goal.conjunction_tac THEN
     REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI THEN' dtac ctxt (rel_sel RS iffD1) THEN'
diff -r f122140b7195 -r c09598a97436 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sat Jul 18 21:25:55 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sat Jul 18 21:44:18 2015 +0200
@@ -117,7 +117,7 @@
   dtac ctxt (coalg_def RS iffD1) 1 THEN
   REPEAT_DETERM (etac ctxt conjE 1) THEN
   EVERY' [dtac ctxt rev_bspec, assume_tac ctxt] 1 THEN
-  REPEAT_DETERM (eresolve0_tac [CollectE, conjE] 1) THEN assume_tac ctxt 1;
+  REPEAT_DETERM (eresolve_tac ctxt [CollectE, conjE] 1) THEN assume_tac ctxt 1;
 
 fun mk_mor_elim_tac ctxt mor_def =
   (dtac ctxt (mor_def RS iffD1) THEN'
@@ -226,7 +226,7 @@
     fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
       EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, dtac ctxt (mk_conjunctN n i),
         etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, etac ctxt bexE,
-        REPEAT_DETERM o eresolve0_tac [CollectE, conjE],
+        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
         rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI),
         CONJ_WRAP' (fn thm => EVERY' [rtac ctxt trans, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt map_cong0,
           REPEAT_DETERM_N m o rtac ctxt thm, REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
@@ -246,7 +246,7 @@
       EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
         etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt,
         dtac ctxt (in_rel RS @{thm iffD1}),
-        REPEAT_DETERM o eresolve0_tac ([CollectE, conjE, exE] @
+        REPEAT_DETERM o eresolve_tac ctxt ([CollectE, conjE, exE] @
           @{thms CollectE Collect_split_in_rel_leE}),
         rtac ctxt bexI, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
         REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
@@ -654,7 +654,7 @@
 
 fun mk_congruent_str_final_tac ctxt m lsbisE map_comp_id map_cong0 equiv_LSBISs =
   EVERY' [rtac ctxt @{thm congruentI}, dtac ctxt lsbisE,
-    REPEAT_DETERM o eresolve0_tac [CollectE, conjE, bexE], rtac ctxt (o_apply RS trans),
+    REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, bexE], rtac ctxt (o_apply RS trans),
     etac ctxt (sym RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans),
     rtac ctxt (map_cong0 RS trans), REPEAT_DETERM_N m o rtac ctxt refl,
     EVERY' (map (fn equiv_LSBIS =>
diff -r f122140b7195 -r c09598a97436 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sat Jul 18 21:25:55 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sat Jul 18 21:44:18 2015 +0200
@@ -126,7 +126,7 @@
     fun mor_tac (set_map, map_comp_id) =
       EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt trans,
         rtac ctxt trans, dtac ctxt rev_bspec, assume_tac ctxt, etac ctxt arg_cong,
-         REPEAT o eresolve0_tac [CollectE, conjE], etac ctxt bspec, rtac ctxt CollectI] THEN'
+         REPEAT o eresolve_tac ctxt [CollectE, conjE], etac ctxt bspec, rtac ctxt CollectI] THEN'
       CONJ_WRAP' (fn thm =>
         FIRST' [rtac ctxt subset_UNIV,
           (EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm image_subsetI},
@@ -172,14 +172,14 @@
         rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE}];
     val alg_tac =
       CONJ_WRAP' (fn (set_maps, alg_set) =>
-        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt set_mp,
+        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt set_mp,
           rtac ctxt equalityD1, etac ctxt @{thm bij_betw_imageE[OF bij_betw_the_inv_into]},
           rtac ctxt imageI, etac ctxt alg_set, EVERY' (map set_tac (drop m set_maps))])
       (set_mapss ~~ alg_sets);
 
     val mor_tac = rtac ctxt conjI THEN' CONJ_WRAP' (K (etac ctxt @{thm bij_betwE})) alg_sets THEN'
       CONJ_WRAP' (fn (set_maps, alg_set) =>
-        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE],
+        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
           etac ctxt @{thm f_the_inv_into_f_bij_betw}, etac ctxt alg_set,
           EVERY' (map set_tac (drop m set_maps))])
       (set_mapss ~~ alg_sets);
@@ -257,7 +257,7 @@
       rtac ctxt @{thm csum_absorb1}, rtac ctxt Asuc_Cinfinite, rtac ctxt @{thm ctwo_ordLeq_Cinfinite},
       rtac ctxt Asuc_Cinfinite, rtac ctxt bd_Card_order,
       rtac ctxt @{thm ordIso_imp_ordLeq}, rtac ctxt @{thm cexp_cprod_ordLeq},
-      resolve0_tac @{thms Card_order_csum Card_order_ctwo}, rtac ctxt suc_Cinfinite,
+      resolve_tac ctxt @{thms Card_order_csum Card_order_ctwo}, rtac ctxt suc_Cinfinite,
       rtac ctxt bd_Cnotzero, rtac ctxt @{thm cardSuc_ordLeq}, rtac ctxt bd_Card_order, rtac ctxt Asuc_Cinfinite];
   in
     (rtac ctxt induct THEN'
@@ -276,7 +276,7 @@
 
     fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ctxt ord_eq_le_trans, etac ctxt min_alg,
       rtac ctxt @{thm Un_least}, minG_tac, rtac ctxt @{thm image_subsetI},
-      REPEAT_DETERM o eresolve0_tac [CollectE, conjE], etac ctxt alg_set,
+      REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], etac ctxt alg_set,
       REPEAT_DETERM o (etac ctxt subset_trans THEN' minG_tac)];
   in
     (rtac ctxt induct THEN'
@@ -290,9 +290,9 @@
     val n = length min_algs;
     fun mk_cardSuc_UNION_tac set_bds (mono, def) = EVERY'
       [rtac ctxt bexE, rtac ctxt @{thm cardSuc_UNION_Cinfinite}, rtac ctxt bd_Cinfinite, rtac ctxt mono,
-       etac ctxt (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve0_tac set_bds];
+       etac ctxt (def RSN (2, @{thm subset_trans[OF _ equalityD1]})), resolve_tac ctxt set_bds];
     fun mk_conjunct_tac (set_bds, (min_alg, min_alg_def)) =
-      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE],
+      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
         EVERY' (map (mk_cardSuc_UNION_tac set_bds) (min_alg_monos ~~ min_alg_defs)), rtac ctxt bexE,
         rtac ctxt bd_limit, REPEAT_DETERM_N (n - 1) o etac ctxt conjI, assume_tac ctxt,
         rtac ctxt (min_alg_def RS @{thm set_mp[OF equalityD2]}),
@@ -339,9 +339,9 @@
     val mor_tac =
       CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs;
     fun alg_epi_tac ((alg_set, str_init_def), set_map) =
-      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt CollectI,
+      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI,
         rtac ctxt ballI, ftac ctxt (alg_select RS bspec), rtac ctxt (str_init_def RS @{thm ssubst_mem}),
-        etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve0_tac set_map,
+        etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve_tac ctxt set_map,
           rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec,
           assume_tac ctxt]];
   in
@@ -358,7 +358,7 @@
     EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
       REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp, rtac ctxt copy,
       REPEAT_DETERM_N n o assume_tac ctxt,
-      rtac ctxt impI, REPEAT_DETERM o eresolve0_tac [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
+      rtac ctxt impI, REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
       rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI,
       rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
       SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)),
@@ -381,7 +381,7 @@
 
     fun mk_alg_tac (ct, (alg_set, (in_mono, (morE, map_cong0)))) =
       EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
-        REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
+        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
         REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
         rtac ctxt trans, mor_tac morE in_mono,
         rtac ctxt trans, cong_tac ct map_cong0,
@@ -400,7 +400,7 @@
     val n = length least_min_algs;
 
     fun mk_alg_tac alg_set = EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
-      REPEAT_DETERM o eresolve0_tac [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
+      REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt conjI, rtac ctxt (alg_min_alg RS alg_set),
       REPEAT_DETERM_N n o (etac ctxt subset_trans THEN' rtac ctxt @{thm Collect_restrict}),
       rtac ctxt mp, etac ctxt bspec, rtac ctxt CollectI,
       REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt),
@@ -449,7 +449,7 @@
   let
     fun mk_unique type_def =
       EVERY' [rtac ctxt @{thm surj_fun_eq}, rtac ctxt (type_def RS @{thm type_definition.Abs_image}),
-        rtac ctxt ballI, resolve0_tac init_unique_mors,
+        rtac ctxt ballI, resolve_tac ctxt init_unique_mors,
         EVERY' (map (fn thm => assume_tac ctxt ORELSE' rtac ctxt thm) Reps),
         rtac ctxt mor_comp, rtac ctxt mor_Abs, assume_tac ctxt,
         rtac ctxt mor_comp, rtac ctxt mor_Abs, rtac ctxt mor_fold];
diff -r f122140b7195 -r c09598a97436 src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sat Jul 18 21:25:55 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sat Jul 18 21:44:18 2015 +0200
@@ -87,7 +87,7 @@
 
 fun mk_exhaust_sel_tac ctxt n exhaust_disc collapses =
   mk_exhaust_disc_or_sel_tac ctxt n exhaust_disc collapses ORELSE
-  HEADGOAL (etac ctxt meta_mp THEN' resolve0_tac collapses);
+  HEADGOAL (etac ctxt meta_mp THEN' resolve_tac ctxt collapses);
 
 fun mk_collapse_tac ctxt m discD sels =
   HEADGOAL (dtac ctxt discD THEN'
diff -r f122140b7195 -r c09598a97436 src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sat Jul 18 21:25:55 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sat Jul 18 21:44:18 2015 +0200
@@ -149,7 +149,7 @@
           NONE => NONE
         | SOME u' => SOME (apply2 (Thm.cterm_of ctxt) (t |> getP |> snd |> head_of, u'))));
     val indrule' = cterm_instantiate insts indrule;
-  in resolve0_tac [indrule'] i end);
+  in resolve_tac ctxt [indrule'] i end);
 
 
 (* perform exhaustive case analysis on last parameter of subgoal i *)
diff -r f122140b7195 -r c09598a97436 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Jul 18 21:25:55 2015 +0200
+++ b/src/Provers/classical.ML	Sat Jul 18 21:44:18 2015 +0200
@@ -157,7 +157,7 @@
       val rule'' =
         rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
           if i = 1 orelse redundant_hyp goal
-          then eresolve0_tac [thin_rl] i
+          then eresolve_tac ctxt [thin_rl] i
           else all_tac))
         |> Seq.hd
         |> Drule.zero_var_indexes;