| changeset 33670 | 02b7738aef6a | 
| parent 33666 | e49bfeb0d822 | 
| child 33671 | 4b0f2599ed48 | 
--- a/src/HOL/Tools/quickcheck_generators.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/HOL/Tools/quickcheck_generators.ML Fri Nov 13 20:41:29 2009 +0100 @@ -214,7 +214,7 @@ lthy |> random_aux_primrec_multi (name ^ prfx) proto_eqs |-> (fn proto_simps => prove_simps proto_simps) - |-> (fn simps => LocalTheory.note "" + |-> (fn simps => LocalTheory.note ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]), simps)) |> snd