src/HOL/ex/Quickcheck.thy
changeset 28360 cf3542e34726
parent 28335 25326092cf9a
child 28370 37f56e6e702d
--- 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