diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Aug 29 12:28:48 2000 +0200
+++ b/src/Pure/library.ML	Tue Aug 29 15:13:10 2000 +0200
@@ -188,6 +188,7 @@
   val assoc2: (''a * (''b * 'c) list) list * (''a * ''b) -> 'c option
   val gen_assoc: ('a * 'b -> bool) -> ('b * 'c) list * 'a -> 'c option
   val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
+  val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
   val gen_overwrite: ('a * 'a -> bool) -> ('a * 'b) list * ('a * 'b) -> ('a * 'b) list
 
   (*generic tables*)
@@ -1204,6 +1205,10 @@
 
 (** misc **)
 
+fun overwrite_warn (args as (alist,(a,_))) text =
+  (if is_none(assoc(alist,a)) then () else warning text;
+   overwrite args);
+
 (*use the keyfun to make a list of (x, key) pairs*)
 fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list =
   let fun keypair x = (x, keyfun x)