locally inverting previously applied simplifications with ex_simps in set_comprehension_pointfree

--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Fri Oct 19 21:52:45 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Oct 18 10:06:27 2012 +0200
@@ -352,7 +352,8 @@
 
 (* main simprocs *)
 
-val prep_thms = map mk_meta_eq [@{thm Bex_def}, @{thm Pow_iff[symmetric]}]
+val prep_thms =
+  map mk_meta_eq ([@{thm Bex_def}, @{thm Pow_iff[symmetric]}] @ @{thms ex_simps[symmetric]})
 
 val post_thms =
   map mk_meta_eq [@{thm Times_Un_distrib1[symmetric]},