1.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Mar 30 08:19:29 2012 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Mar 30 08:19:31 2012 +0200
     1.3 @@ -419,10 +419,9 @@
     1.4            (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t
     1.5        in
     1.6          fold (fn (name, eq) => Local_Theory.note
     1.7 -          ((Binding.conceal
     1.8 -            (Binding.qualify true prfx
     1.9 -              (Binding.qualify true name (Binding.name "simps"))),
    1.10 -             Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), [eq]) #> snd)
    1.11 +          ((Binding.qualify true prfx
    1.12 +              (Binding.qualify true name (Binding.name "simps")),
    1.13 +             [Code.add_default_eqn_attrib]), [eq]) #> snd)
    1.14            (names ~~ eqs) lthy
    1.15        end)
    1.16