src/HOL/Tools/Quickcheck/random_generators.ML

   in
     lthy
     |> 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
 
 
 (* constructing random instances on datatypes *)