# HG changeset patch
# User bulwahn
# Date 1350547587 -7200
# Node ID 50e457bbc5fe40de8f43f4daa578b99302795902
# Parent  f2db0596bd611aa108894ad1cedb95a73c6a9738
locally inverting previously applied simplifications with ex_simps in set_comprehension_pointfree

diff -r f2db0596bd61 -r 50e457bbc5fe src/HOL/Tools/set_comprehension_pointfree.ML
--- 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]},