src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Sat May 16 10:19:01 2009 +0200
+++ b/src/HOL/HOL.thy	Sat May 16 15:23:52 2009 +0200
@@ -1988,6 +1988,18 @@
 
 subsubsection {* Quickcheck *}
 
+ML {*
+structure Quickcheck_RecFun_Simp_Thms = NamedThmsFun
+(
+  val name = "quickcheck_recfun_simp"
+  val description = "simplification rules of recursive functions as needed by Quickcheck"
+)
+*}
+
+setup {*
+  Quickcheck_RecFun_Simp_Thms.setup
+*}
+
 setup {*
   Quickcheck.add_generator ("SML", Codegen.test_term)
 *}