# HG changeset patch
# User bulwahn
# Date 1333088371 -7200
# Node ID 6212bcc94bb08ca2ddb9004af734831127da93bb
# Parent  ac625d8346b2e5b30d7c72c97afe3346b0d58f5e
refine bindings in quickcheck_common: do not conceal and do not declare as simps

diff -r ac625d8346b2 -r 6212bcc94bb0 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)