--- a/src/HOL/Tools/Quickcheck/random_generators.ML Sat Nov 19 17:20:17 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sat Nov 19 21:18:38 2011 +0100
@@ -171,8 +171,7 @@
|> random_aux_primrec_multi (name ^ prfx) proto_eqs
|-> (fn proto_simps => prove_simps proto_simps)
|-> (fn simps => Local_Theory.note
- ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Simps.add]), simps))
+ ((b, Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), simps))
|> snd
end