refine bindings in quickcheck_common: do not conceal and do not declare as simps
authorbulwahn
Fri, 30 Mar 2012 08:19:31 +0200
changeset 47204 6212bcc94bb0
parent 47203 ac625d8346b2
child 47205 34e8b7347dda
refine bindings in quickcheck_common: do not conceal and do not declare as simps
src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- 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)