src/HOL/Tools/quickcheck_generators.ML
changeset 31902 862ae16a799d
parent 31868 edd1f30c0477
child 31933 cd6511035315
     1.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Thu Jul 02 17:33:36 2009 +0200
     1.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Jul 02 17:34:14 2009 +0200
     1.3 @@ -244,7 +244,7 @@
     1.4      |-> (fn proto_simps => prove_simps proto_simps)
     1.5      |-> (fn simps => LocalTheory.note Thm.generatedK ((b,
     1.6             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
     1.7 -          [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]),
     1.8 +          [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]),
     1.9              simps))
    1.10      |> snd
    1.11    end