--- a/src/HOL/Tools/Quickcheck/random_generators.ML Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sun Jul 02 20:13:38 2017 +0200
@@ -179,8 +179,8 @@
|> random_aux_primrec_multi (name ^ prfx) proto_eqs
|-> prove_simps
|-> (fn simps => Local_Theory.note
- ((b, Code.add_default_eqn_attrib Code.Equation:: @{attributes [simp, nitpick_simp]}), simps))
- |> snd
+ ((b, @{attributes [simp, nitpick_simp]}), simps))
+ |-> (fn (_, thms) => Code.declare_default_eqns (map (rpair true) thms))
end