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