src/HOL/Tools/quickcheck_generators.ML
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