--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Jan 29 15:05:53 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Jan 29 16:35:05 2014 +0100
@@ -189,9 +189,10 @@
unfold_tac ctxt [in_rel] THEN
REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN
hyp_subst_tac ctxt 1 THEN
- unfold_tac ctxt set_maps THEN
EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]},
- CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1;
+ CONJ_WRAP' (fn thm =>
+ (etac (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' atac))
+ set_maps] 1;
fun mk_map_transfer_tac rel_mono in_rel set_maps map_cong0 map_comp
{context = ctxt, prems = _} =