--- a/src/HOL/Tools/recdef_package.ML Tue Feb 10 14:20:47 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML Tue Feb 10 14:58:15 2009 +0100
@@ -207,7 +207,8 @@
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, Code.add_default_eqn_attribute] else [];
+ val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
+ Code.add_default_eqn_attribute] else [];
val ((simps' :: rules', [induct']), thy) =
thy