TFL/tfl.sml
changeset 9721 7e51c9f3d5a0
parent 9651 f0cfddda6038
child 9763 252c690690b0
--- a/TFL/tfl.sml	Tue Aug 29 12:28:48 2000 +0200
+++ b/TFL/tfl.sml	Tue Aug 29 15:13:10 2000 +0200
@@ -47,9 +47,8 @@
 
 fun add_cong(congs,thm) =
   let val c = cong_hd thm
-  in case assoc(congs,c) of None => (c,thm)::congs
-     | _ => (warning ("Overwriting congruence rule for " ^ quote c);
-             overwrite (congs, (c,thm)))
+  in overwrite_warn (congs,(c,thm))
+       ("Overwriting congruence rule for " ^ quote c)
   end
 
 fun del_cong(congs,thm) =