--- a/src/HOL/Tools/quickcheck_generators.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Thu Jul 02 17:34:14 2009 +0200
@@ -244,7 +244,7 @@
|-> (fn proto_simps => prove_simps proto_simps)
|-> (fn simps => LocalTheory.note Thm.generatedK ((b,
Code.add_default_eqn_attrib :: map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]),
+ [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]),
simps))
|> snd
end