# HG changeset patch
# User haftmann
# Date 1127458819 -7200
# Node ID 01870f76478c8980e4004bbce494a77815941927
# Parent  ece268908438b29288dbe0858f7299afdba0e5f8
temporarily re-introduced overwrite_warn

diff -r ece268908438 -r 01870f76478c src/HOL/Tools/recdef_package.ML
--- 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