# 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