# HG changeset patch # User bulwahn # Date 1327323979 -3600 # Node ID 518cc38a1a8c83fa65e691bf81776461bc73338a # Parent 56fae81902ce254baec7f7b39e3727e20c66274a adding fun_eq_iff to the preprocessing diff -r 56fae81902ce -r 518cc38a1a8c src/HOL/Tools/Quickcheck/quickcheck_common.ML --- 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