src/HOL/Tools/quickcheck_generators.ML
changeset 33666 e49bfeb0d822
parent 33553 35f2b30593a8
child 33670 02b7738aef6a
     1.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 15:48:52 2009 +0100
     1.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 17:25:09 2009 +0100
     1.3 @@ -214,8 +214,8 @@
     1.4      lthy
     1.5      |> random_aux_primrec_multi (name ^ prfx) proto_eqs
     1.6      |-> (fn proto_simps => prove_simps proto_simps)
     1.7 -    |-> (fn simps => LocalTheory.note Thm.generatedK ((b,
     1.8 -           Code.add_default_eqn_attrib :: map (Attrib.internal o K)
     1.9 +    |-> (fn simps => LocalTheory.note ""
    1.10 +      ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K)
    1.11            [Simplifier.simp_add, Nitpick_Simps.add]), simps))
    1.12      |> snd
    1.13    end