--- 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