--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Jan 23 15:22:33 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Jan 23 15:23:02 2012 +0100
@@ -388,7 +388,8 @@
map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
(@{thms all_simps} @ @{thms ex_simps})
@ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
- [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all}]
+ [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all},
+ @{thm meta_eq_to_obj_eq [OF Ex1_def]}]
fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t