# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1391015386 0
# Node ID 4d80d91cb447437434873418cc3ca3015121894b
# Parent  f4791db200671ac604f926aaf525dd1340f19bab# Parent  409b2b2e7c5a932532be74e159be11bff55fd809
Merge

diff -r f4791db20067 -r 4d80d91cb447 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Wed Jan 29 17:09:01 2014 +0000
+++ b/src/HOL/BNF_Def.thy	Wed Jan 29 17:09:46 2014 +0000
@@ -110,10 +110,11 @@
   by auto
 
 lemma Collect_split_mono_strong: 
-  "\<lbrakk>\<forall>a\<in>fst ` A. \<forall>b \<in> snd ` A. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (split P)\<rbrakk> \<Longrightarrow>
+  "\<lbrakk>X = fst ` A; Y = snd ` A; \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (split P)\<rbrakk> \<Longrightarrow>
   A \<subseteq> Collect (split Q)"
   by fastforce
 
+
 lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
 by metis
 
diff -r f4791db20067 -r 4d80d91cb447 src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Wed Jan 29 17:09:01 2014 +0000
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Wed Jan 29 17:09:46 2014 +0000
@@ -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 = _} =