--- a/src/HOL/Tools/recdef_package.ML Fri Sep 23 00:52:13 2005 +0200
+++ b/src/HOL/Tools/recdef_package.ML Fri Sep 23 09:00:19 2005 +0200
@@ -82,7 +82,8 @@
fun add_cong raw_thm congs =
let val (c, thm) = prep_cong raw_thm
- in update_warn (op =) ("Overwriting recdef congruence rule for " ^ quote c) (c, thm) congs end;
+(* in update_warn (op =) ("Overwriting recdef congruence rule for " ^ quote c) (c, thm) congs end; *)
+ in overwrite_warn (congs, (c, thm)) ("Overwriting recdef congruence rule for " ^ quote c) end;
fun del_cong raw_thm congs =
let