--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Jan 23 14:00:52 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Jan 23 14:06:19 2012 +0100
@@ -262,7 +262,7 @@
val thy = Proof_Context.theory_of ctxt
val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
val rewrs = map (swap o dest) @{thms all_simps} @
- (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}])
+ (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff}])
val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t)
val (vs, body) = strip_all t'
val vs' = Variable.variant_frees ctxt [t'] vs