# HG changeset patch
# User haftmann
# Date 1222362950 -7200
# Node ID cf3542e34726e22cee3fa0b0a28d21916914424b
# Parent  bd4750bcb4e67c7fafa02337a605f964ffafab89
circumvent problem with code redundancy

diff -r bd4750bcb4e6 -r cf3542e34726 src/HOL/ex/Quickcheck.thy
--- a/src/HOL/ex/Quickcheck.thy	Thu Sep 25 16:05:52 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy	Thu Sep 25 19:15:50 2008 +0200
@@ -137,10 +137,13 @@
               val thm = @{thm random'_if}
                 |> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')]
                 |> (fn thm => thm OF simps)
-                |> singleton (ProofContext.export lthy (ProofContext.init thy))
+                |> singleton (ProofContext.export lthy (ProofContext.init thy));
+              val c = (fst o dest_Const o fst o strip_comb o fst
+                o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm;
             in
               lthy
-              |> LocalTheory.theory (PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal])
+              |> LocalTheory.theory (Code.del_funcs c
+                   #> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal])
                    #-> Code.add_func)
             end;
         in