--- a/src/HOL/Tools/quickcheck_generators.ML Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Wed Oct 21 17:34:35 2009 +0200
@@ -214,7 +214,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_Simps.add, Quickcheck_RecFun_Simps.add]),
+ [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]),
simps))
|> snd
end