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) =