# HG changeset patch
# User traytel
# Date 1391009705 -3600
# Node ID a740f312d9e49cdb6bb5c1e4be558b399f06b902
# Parent  2d69438b1b0cb6ce8472e409f1fb28b9ce73ef53
made tactic more robust

diff -r 2d69438b1b0c -r a740f312d9e4 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Wed Jan 29 15:05:53 2014 +0100
+++ b/src/HOL/BNF_Def.thy	Wed Jan 29 16:35:05 2014 +0100
@@ -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 2d69438b1b0c -r a740f312d9e4 src/HOL/Tools/BNF/bnf_def_tactics.ML
--- 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 = _} =