# HG changeset patch
# User bulwahn
# Date 1349858872 -7200
# Node ID b9eb9c2b87c70be07f8b58bb940c284d992abf4d
# Parent  9979d64b80169ea3e99c867bdadd4b099a1648cc
unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc

diff -r 9979d64b8016 -r b9eb9c2b87c7 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 10 10:47:43 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 10 10:47:52 2012 +0200
@@ -133,10 +133,15 @@
 
 fun conv ctxt t =
   let
-    fun mk_thm t' = Goal.prove ctxt [] []
-      (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) (K (tac 1));
+    val ct = cterm_of (Proof_Context.theory_of ctxt) t
+    val Bex_def = mk_meta_eq @{thm Bex_def}
+    val unfold_eq = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv Bex_def))) ctxt ct
+    val t' = term_of (Thm.rhs_of unfold_eq) 
+    fun mk_thm t'' = Goal.prove ctxt [] []
+      (HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (K (tac 1))
+    fun unfold th = th RS ((unfold_eq RS meta_eq_to_obj_eq) RS @{thm trans})
   in
-    Option.map mk_thm (rewrite_term t)
+    Option.map (unfold o mk_thm) (rewrite_term t')
   end;
 
 (* simproc *)