# HG changeset patch
# User haftmann
# Date 1127316332 -7200
# Node ID 7322f37d334473f9b19c2c1a8369aa0314ad6ce9
# Parent  0350ac95c4b6f0a00aa62d0bd2a97439313a04e7
introduces update_warn instead of overwrite_warn

diff -r 0350ac95c4b6 -r 7322f37d3344 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Wed Sep 21 17:21:35 2005 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Wed Sep 21 17:25:32 2005 +0200
@@ -82,7 +82,7 @@
 
 fun add_cong raw_thm congs =
   let val (c, thm) = prep_cong raw_thm
-  in overwrite_warn (congs, (c, thm)) ("Overwriting recdef congruence rule for " ^ quote c) end;
+  in update_warn (op =) ("Overwriting recdef congruence rule for " ^ quote c) (c, thm) congs end;
 
 fun del_cong raw_thm congs =
   let