src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 46316 1c9a548c0402
parent 46309 693d8d7bc3cd
child 46335 0fd9ab902b5a
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jan 23 15:22:33 2012 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jan 23 15:23:02 2012 +0100
     1.3 @@ -388,7 +388,8 @@
     1.4      map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
     1.5        (@{thms all_simps} @ @{thms ex_simps})
     1.6      @ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
     1.7 -        [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all}]
     1.8 +        [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all},
     1.9 +         @{thm meta_eq_to_obj_eq [OF Ex1_def]}]
    1.10  
    1.11  fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t
    1.12