--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Tue Feb 10 14:48:26 2015 +0100
@@ -201,19 +201,20 @@
in
EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps},
in_rel_of_bnf bnf, pred_def]), rtac iffI,
- REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt,
+ REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], hyp_subst_tac ctxt,
CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp),
etac imageE, dtac set_rev_mp, assume_tac ctxt,
- REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}],
+ REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm case_prodE}],
hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]},
etac @{thm DomainPI}]) set_map's,
- REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI],
+ REPEAT_DETERM o etac conjE,
+ REPEAT_DETERM o resolve_tac ctxt [exI, (refl RS conjI), rotate_prems 1 conjI],
rtac refl, rtac (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym,
map_id_of_bnf bnf]),
REPEAT_DETERM_N n o (EVERY' [rtac @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]},
rtac @{thm fst_conv}]), rtac CollectI,
CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}),
- REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
+ REPEAT_DETERM o resolve_tac ctxt [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
dtac (rotate_prems 1 bspec), assume_tac ctxt,
etac @{thm DomainpE}, etac @{thm someI}]) set_map's
] i