diff -r beb26c5901f3 -r 74d72ba262fb src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Sat May 16 10:19:01 2009 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Sat May 16 15:23:52 2009 +0200
@@ -208,7 +208,7 @@
                congs wfs name R eqs;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
-      Code.add_default_eqn_attribute] else [];
+      Code.add_default_eqn_attribute, Quickcheck_RecFun_Simp_Thms.add] else [];
 
     val ((simps' :: rules', [induct']), thy) =
       thy