# HG changeset patch
# User wenzelm
# Date 1257863615 -3600
# Node ID 506f80a9afe805bf7a4c0ac37e2ab25bef15ec90
# Parent  c40ced05b10ab4873f581623e0adcddbfac874ad
removed unused Quickcheck_RecFun_Simps;

diff -r c40ced05b10a -r 506f80a9afe8 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Nov 10 15:32:43 2009 +0100
+++ b/src/HOL/HOL.thy	Tue Nov 10 15:33:35 2009 +0100
@@ -2003,16 +2003,6 @@
 
 quickcheck_params [size = 5, iterations = 50]
 
-ML {*
-structure Quickcheck_RecFun_Simps = Named_Thms
-(
-  val name = "quickcheck_recfun_simp"
-  val description = "simplification rules of recursive functions as needed by Quickcheck"
-)
-*}
-
-setup Quickcheck_RecFun_Simps.setup
-
 
 subsubsection {* Nitpick setup *}
 
diff -r c40ced05b10a -r 506f80a9afe8 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Tue Nov 10 15:32:43 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Tue Nov 10 15:33:35 2009 +0100
@@ -37,8 +37,7 @@
 val simp_attribs = map (Attrib.internal o K)
     [Simplifier.simp_add,
      Code.add_default_eqn_attribute,
-     Nitpick_Simps.add,
-     Quickcheck_RecFun_Simps.add]
+     Nitpick_Simps.add]
 
 val psimp_attribs = map (Attrib.internal o K)
     [Simplifier.simp_add,
diff -r c40ced05b10a -r 506f80a9afe8 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Tue Nov 10 15:32:43 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Tue Nov 10 15:33:35 2009 +0100
@@ -270,9 +270,9 @@
     val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
     fun attr_bindings prefix = map (fn ((b, attrs), _) =>
       (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
-    fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"),
-      map (Attrib.internal o K)
-        [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]);
+    fun simp_attr_binding prefix =
+      (Binding.qualify true prefix (Binding.name "simps"),
+        map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]);
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial ())
diff -r c40ced05b10a -r 506f80a9afe8 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Tue Nov 10 15:32:43 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Nov 10 15:33:35 2009 +0100
@@ -216,8 +216,7 @@
     |-> (fn proto_simps => prove_simps proto_simps)
     |-> (fn simps => LocalTheory.note Thm.generatedK ((b,
            Code.add_default_eqn_attrib :: map (Attrib.internal o K)
-          [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]),
-            simps))
+          [Simplifier.simp_add, Nitpick_Simps.add]), simps))
     |> snd
   end
 
diff -r c40ced05b10a -r 506f80a9afe8 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Tue Nov 10 15:32:43 2009 +0100
+++ b/src/HOL/Tools/recdef.ML	Tue Nov 10 15:33:35 2009 +0100
@@ -201,8 +201,9 @@
         tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
                congs wfs name R eqs;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
-    val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Simps.add,
-      Code.add_default_eqn_attribute, Quickcheck_RecFun_Simps.add] else [];
+    val simp_att =
+      if null tcs then [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]
+      else [];
 
     val ((simps' :: rules', [induct']), thy) =
       thy