src/HOL/Tools/BNF/bnf_gfp_tactics.ML

   val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list ->
     thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list ->
     thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
     thm list list -> thm list -> thm list -> tactic
   val mk_mor_case_sum_tac: 'a list -> thm -> tactic
-  val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
+  val mk_mor_comp_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
   val mk_mor_elim_tac: thm -> tactic
   val mk_mor_col_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
     thm list -> thm list list -> thm list list -> tactic
   val mk_mor_incl_tac: thm -> thm list -> tactic
   val mk_mor_str_tac: 'a list -> thm -> tactic

 
 fun mk_coalg_set_tac coalg_def =
   dtac (coalg_def RS iffD1) 1 THEN
   REPEAT_DETERM (etac conjE 1) THEN
   EVERY' [dtac rev_bspec, atac] 1 THEN
-  REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
+  REPEAT_DETERM (eresolve0_tac [CollectE, conjE] 1) THEN atac 1;
 
 fun mk_mor_elim_tac mor_def =
   (dtac (mor_def RS iffD1) THEN'
   REPEAT o etac conjE THEN'
   TRY o rtac @{thm image_subsetI} THEN'

   CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, etac (id_apply RS @{thm ssubst_mem})]))
     map_ids THEN'
   CONJ_WRAP' (fn thm =>
     (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_ids) 1;
 
-fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids =
+fun mk_mor_comp_tac ctxt mor_def mor_images morEs map_comp_ids =
   let
     fun fbetw_tac image = EVERY' [rtac ballI, rtac (o_apply RS @{thm ssubst_mem}), etac image,
       etac image, atac];
     fun mor_tac ((mor_image, morE), map_comp_id) =
-      EVERY' [rtac ballI, stac o_apply, rtac trans, rtac (map_comp_id RS sym), rtac trans,
+      EVERY' [rtac ballI, stac ctxt o_apply, rtac trans, rtac (map_comp_id RS sym), rtac trans,
         etac (morE RS arg_cong), atac, etac morE, etac mor_image, atac];
   in
     (rtac (mor_def RS iffD2) THEN' rtac conjI THEN'
     CONJ_WRAP' fbetw_tac mor_images THEN'
     CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1

     CONJ_WRAP' (fn rec_Suc => EVERY'
       [rtac ord_eq_le_trans, rtac rec_Suc,
         if m = 0 then K all_tac
         else (rtac @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),
         CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
-          (K (EVERY' [rtac @{thm UN_least}, REPEAT_DETERM o eresolve_tac [allE, conjE],
+          (K (EVERY' [rtac @{thm UN_least}, REPEAT_DETERM o eresolve_tac ctxt [allE, conjE],
             rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])
       rec_Sucs] 1;
 
 fun mk_Jset_minimal_tac ctxt n col_minimal =
   (CONJ_WRAP' (K (EVERY' [rtac @{thm UN_least}, rtac rev_mp, rtac col_minimal,
     EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
-    REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) (1 upto n)) 1
+    REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], atac])) (1 upto n)) 1
 
 fun mk_mor_col_tac m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss =
   EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
     REPEAT_DETERM o rtac allI,
     CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s,

     val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ in_rels);
 
     fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
       EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
         etac allE, etac allE, etac impE, atac, etac bexE,
-        REPEAT_DETERM o eresolve_tac [CollectE, conjE],
+        REPEAT_DETERM o eresolve0_tac [CollectE, conjE],
         rtac (in_rel RS iffD2), rtac exI, rtac (Drule.rotate_prems 1 conjI),
         CONJ_WRAP' (fn thm => EVERY' [rtac trans, rtac trans, rtac map_comp0, rtac map_cong0,
           REPEAT_DETERM_N m o rtac thm, REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
           atac])
         @{thms fst_diag_id snd_diag_id},

 
     fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
       EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
         etac allE, etac allE, etac impE, atac,
         dtac (in_rel RS @{thm iffD1}),
-        REPEAT_DETERM o eresolve_tac ([CollectE, conjE, exE] @
+        REPEAT_DETERM o eresolve0_tac ([CollectE, conjE, exE] @
           @{thms CollectE Collect_split_in_rel_leE}),
         rtac bexI, rtac conjI, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
         REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
         REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
         atac, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,

 fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong =
   let
     val n = length lsbis_defs;
   in
     EVERY' [rtac (Thm.permute_prems 0 1 bis_cong), EVERY' (map rtac lsbis_defs),
-      rtac bis_Union, rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE, exE],
+      rtac bis_Union, rtac ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, exE],
       hyp_subst_tac ctxt, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
   end;
 
 fun mk_incl_lsbis_tac n i lsbis_def =
   EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm SUP_upper2}, rtac CollectI,

 fun mk_coalgT_tac ctxt m defs strT_defs set_map0ss =
   let
     val n = length strT_defs;
     val ks = 1 upto n;
     fun coalg_tac (i, (active_sets, def)) =
-      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
+      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE],
         hyp_subst_tac ctxt, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
         rtac (mk_sum_caseN n i), rtac CollectI,
         REPEAT_DETERM_N m o EVERY' [rtac conjI, rtac subset_UNIV],
         CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS ord_eq_le_trans),
           rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,

             etac equalityD1, etac CollectD,
           rtac ballI,
             CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD},
               dtac bspec, etac thin_rl, atac, dtac (mk_conjunctN n i),
               dtac bspec, rtac CollectI, etac @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
-              REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
+              REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac exI,
               rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
               rtac (@{thm append_Cons} RS sym RS arg_cong RS trans), atac,
               CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
                 rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
                 rtac (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
           dtac bspec, atac, dtac (mk_conjunctN n i), dtac bspec,
           etac @{thm set_mp[OF equalityD1]}, atac,
-          REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
+          REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac exI,
           rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
           etac (@{thm append_Nil} RS sym RS arg_cong RS trans),
           REPEAT_DETERM_N m o (rtac conjI THEN' atac),
           CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
             rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},

       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn Lev_Suc =>
         EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn i =>
-              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
+              EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt,
                 rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
                 REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
       Lev_Sucs] 1
   end;
 

       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) =>
         EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn (i, from_to_sbd) =>
-              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
+              EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt,
                 CONJ_WRAP' (fn i' => rtac impI THEN'
                   CONJ_WRAP' (fn i'' =>
                     EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp),
                       rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnIN n i),
                       rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,

               (if i = i''
               then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]},
                 dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i),
                 hyp_subst_tac ctxt,
                 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
-                  (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
+                  (fn k => REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN'
                     dtac list_inject_iffD1 THEN' etac conjE THEN'
                     (if k = i'
                     then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac ctxt, etac imageI]
                     else etac (mk_InN_not_InM i' k RS notE)))
                 (rev ks)]

       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) =>
         EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn (i, (from_to_sbd, to_sbd_inj)) =>
-              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN'
+              REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN'
               CONJ_WRAP' (fn i' => rtac impI THEN'
                 dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
                 dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
                 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k =>
-                  REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
+                  REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN'
                   dtac list_inject_iffD1 THEN' etac conjE THEN'
                   (if k = i
                   then EVERY' [dtac (mk_InN_inject n i),
                     dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
                     atac, atac, hyp_subst_tac ctxt] THEN'

         (**)
           rtac ballI, etac @{thm UN_E},
           CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s,
             (set_Levs, set_image_Levs))))) =>
             EVERY' [rtac ballI,
-              REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
+              REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
               rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS iffD2),
               rtac exI, rtac conjI,
               if n = 1 then rtac refl
               else etac (sum_case_cong_weak RS trans) THEN' rtac (mk_sum_caseN n i),
               CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
                 EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
                   rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
                   if n = 1 then rtac refl else atac, atac, rtac subsetI,
-                  REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
+                  REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
                   REPEAT_DETERM_N 4 o etac thin_rl,
                   rtac set_image_Lev,
                   atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
                   etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
                   if n = 1 then rtac refl else atac])

           CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
             EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
               rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,
               rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, rtac rv_Nil,
               atac, rtac subsetI,
-              REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
+              REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
               rtac set_image_Lev, rtac (Lev_0 RS equalityD2 RS set_mp),
               rtac @{thm singletonI}, dtac length_Lev',
               etac @{thm set_mp[OF equalityD1[OF arg_cong[OF
                 trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
               rtac rv_Nil])

         rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
         EVERY' (@{map 3} (fn i' => fn to_sbd_inj => fn from_to_sbd =>
           DETERM o EVERY' [rtac trans, rtac o_apply, rtac prod_injectI, rtac conjI,
             rtac trans, rtac @{thm Shift_def},
             rtac equalityI, rtac subsetI, etac thin_rl,
-            REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
+            REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
             etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},
             rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
             CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
-              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
+              EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE],
                 dtac list_inject_iffD1, etac conjE,
                 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
                   dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
                   atac, atac, hyp_subst_tac ctxt, etac @{thm UN_I[OF UNIV_I]}]
                 else etac (mk_InN_not_InM i' i'' RS notE)])

           (length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1
   end;
 
 fun mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBISs =
   EVERY' [rtac @{thm congruentI}, dtac lsbisE,
-    REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], rtac (o_apply RS trans),
+    REPEAT_DETERM o eresolve0_tac [CollectE, conjE, bexE], rtac (o_apply RS trans),
     etac (sym RS arg_cong RS trans), rtac (map_comp_id RS trans),
     rtac (map_cong0 RS trans), REPEAT_DETERM_N m o rtac refl,
     EVERY' (map (fn equiv_LSBIS =>
       EVERY' [rtac @{thm equiv_proj}, rtac equiv_LSBIS, etac set_mp, atac])
     equiv_LSBISs), rtac sym, rtac (o_apply RS trans),

     val ks = 1 upto n;
   in
     EVERY' ([rtac rev_mp, coinduct_tac] @
       maps (fn ((((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_Jsets),
         set_Jset_Jsetss), in_rel) =>
-        [REPEAT_DETERM o resolve_tac [allI, impI, in_rel RS iffD2],
-         REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI,
+        [REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2],
+         REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], hyp_subst_tac ctxt, rtac exI,
          rtac (Drule.rotate_prems 1 conjI),
          rtac conjI, rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
          REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm fst_conv}),
          REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
          rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,

       rtac @{thm relcomppI}, etac Jrel_imp_rel, etac Jrel_imp_rel]
     end)
   rel_Jrels le_rel_OOs) 1;
 
 fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits =
-  ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
+  ALLGOALS (TRY o (eresolve_tac ctxt coind_wits THEN' rtac refl)) THEN
   REPEAT_DETERM (atac 1 ORELSE
-    EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
+    EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac ctxt dtor_set,
     K (unfold_thms_tac ctxt dtor_ctors),
     REPEAT_DETERM_N n o etac UnE,
     REPEAT_DETERM o
       (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
-        (eresolve_tac wit ORELSE'
-        (dresolve_tac wit THEN'
+        (eresolve_tac ctxt wit ORELSE'
+        (dresolve_tac ctxt wit THEN'
           (etac FalseE ORELSE'
-          EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
+          EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac ctxt dtor_set,
             K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
 
 fun mk_coind_wit_tac ctxt induct unfolds set_nats wits =
   rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
   ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN
   ALLGOALS (TRY o
-    FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]);
+    FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac ctxt wits THEN' etac FalseE]);
 
 fun mk_dtor_corec_transfer_tac ctxt n m dtor_corec_defs dtor_unfold_transfer pre_T_map_transfers
     dtor_rels =
   CONJ_WRAP (fn (dtor_corec_def, dtor_unfold_transfer) =>
       REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN

     val m = length dtor_set_incls;
     val n = length dtor_set_set_inclss;
     val (passive_set_map0s, active_set_map0s) = chop m set_map0s;
     val in_Jrel = nth in_Jrels (i - 1);
     val if_tac =
-      EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+      EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
         rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
         EVERY' (map2 (fn set_map0 => fn set_incl =>
           EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0,
             rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
             etac (set_incl RS @{thm subset_trans})])

           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
           REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
           rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
         @{thms fst_conv snd_conv}];
     val only_if_tac =
-      EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+      EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
         rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
         CONJ_WRAP' (fn (dtor_set, passive_set_map0) =>
           EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
             rtac ord_eq_le_trans, rtac @{thm box_equals}, rtac passive_set_map0,
             rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,

               (fn (active_set_map0, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
                 rtac @{thm SUP_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
                 rtac active_set_map0, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
                 dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
                 dtac @{thm ssubst_mem[OF pair_collapse]},
-                REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
+                REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
                   @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
                 hyp_subst_tac ctxt,
                 dtac (in_Jrel RS iffD1),
                 dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
-                REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
+                REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], atac])
             (rev (active_set_map0s ~~ in_Jrels))])
         (dtor_sets ~~ passive_set_map0s),
         rtac conjI,
         REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
           rtac @{thm box_equals}, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
           rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
           EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
             dtac @{thm ssubst_mem[OF pair_collapse]},
-            REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
+            REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
               @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
             hyp_subst_tac ctxt, dtac (in_Jrel RS iffD1),
             dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jrels),
           atac]]
   in

     val snd_diag_nth = if fst then @{thm snd_diag_fst} else @{thm snd_diag_snd};
   in
     EVERY' [rtac coinduct,
       EVERY' (@{map 8} (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s =>
           fn dtor_unfold => fn dtor_map => fn in_rel =>
-        EVERY' [REPEAT_DETERM o resolve_tac [allI, impI, in_rel RS iffD2],
-          REPEAT_DETERM o eresolve_tac [exE, conjE],
+        EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2],
+          REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
           select_prem_tac (length ks) (dtac @{thm spec2}) i, dtac mp, atac,
-          REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
+          REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt,
           rtac exI, rtac (Drule.rotate_prems 1 conjI), rtac conjI,
           rtac (map_comp0 RS trans), rtac (dtor_map RS trans RS sym),
           rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp0, map_cong]),
           REPEAT_DETERM_N m o rtac (fst_diag_nth RS @{thm fun_cong[OF trans[OF o_id sym]]}),
           REPEAT_DETERM_N n o (rtac @{thm sym[OF trans[OF o_apply]]} THEN' rtac @{thm fst_conv}),

 fun mk_rel_coinduct_ind_tac ctxt m ks unfolds set_map0ss j set_induct =
   let val n = length ks;
   in
     rtac set_induct 1 THEN
     EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
-      EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
+      EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac conjE,
         select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
-        REPEAT_DETERM o eresolve_tac [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
+        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
         hyp_subst_tac ctxt,
         SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)),
         rtac subset_refl])
     unfolds set_map0ss ks) 1 THEN
     EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
       EVERY' (map (fn set_map0 =>
-        EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
+        EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac conjE,
         select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
-        REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
+        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt,
         SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)),
-        etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [allE, mp],
+        etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp],
         rtac conjI, etac Collect_splitD_set_mp, atac, rtac (@{thm surjective_pairing} RS arg_cong)])
       (drop m set_map0s)))
     unfolds set_map0ss ks) 1
   end;
 

         if null helper_inds then rtac UNIV_I
         else rtac CollectI THEN'
           CONJ_WRAP' (fn helper_ind =>
             EVERY' [rtac (helper_ind RS rev_mp), REPEAT_DETERM_N n o atac,
               REPEAT_DETERM_N n o etac thin_rl, rtac impI,
-              REPEAT_DETERM o resolve_tac [subsetI, CollectI, @{thm iffD2[OF split_beta]}],
-              dtac bspec, atac, REPEAT_DETERM o eresolve_tac [allE, mp, conjE],
+              REPEAT_DETERM o resolve_tac ctxt [subsetI, CollectI, @{thm iffD2[OF split_beta]}],
+              dtac bspec, atac, REPEAT_DETERM o eresolve_tac ctxt [allE, mp, conjE],
               etac (refl RSN (2, conjI))])
           helper_inds,
         rtac conjI,
         rtac (helper_coind1 RS rev_mp), REPEAT_DETERM_N n o atac, REPEAT_DETERM_N n o etac thin_rl,
         rtac impI, etac mp, rtac exI, etac (refl RSN (2, conjI)),

   in
     unfold_thms_tac ctxt
       @{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
     unfold_thms_tac ctxt @{thms rel_fun_iff_geq_image2p} THEN
     HEADGOAL (EVERY'
-      [REPEAT_DETERM o resolve_tac [allI, impI], rtac ctor_rel_coinduct,
+      [REPEAT_DETERM o resolve_tac ctxt [allI, impI], rtac ctor_rel_coinduct,
       EVERY' (map (fn map_transfer => EVERY'
-        [REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt,
+        [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt,
         SELECT_GOAL (unfold_thms_tac ctxt unfolds),
         rtac (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
         REPEAT_DETERM_N m o rtac @{thm id_transfer},
         REPEAT_DETERM_N n o rtac @{thm rel_fun_image2p},
         etac @{thm predicate2D}, etac @{thm image2pI}])