Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
introduces update_warn instead of overwrite_warn
authorhaftmann
Wed, 21 Sep 2005 17:25:32 +0200
changeset 17565 7322f37d3344
parent 17564 0350ac95c4b6
child 17566 484ff733f29c
introduces update_warn instead of overwrite_warn
src/HOL/Tools/recdef_package.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle