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