src/HOL/Tools/Quickcheck/quickcheck_common.ML

         val eqs_t = mk_equations consts
         val eqs = map (fn eq => Goal.prove lthy argnames [] eq
           (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t
       in
         fold (fn (name, eq) => Local_Theory.note
-        ((Binding.conceal (Binding.qualify true prfx
-           (Binding.qualify true name (Binding.name "simps"))),
-           Code.add_default_eqn_attrib :: map (Attrib.internal o K)
-             [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (names ~~ eqs) lthy
+          ((Binding.conceal
+            (Binding.qualify true prfx
+              (Binding.qualify true name (Binding.name "simps"))),
+             Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), [eq]) #> snd)
+          (names ~~ eqs) lthy
       end)
 
 (** ensuring sort constraints **)
 
 fun perhaps_constrain thy insts raw_vs =