combinator for overwriting changes with warning

--- a/src/Pure/General/output.ML	Mon Nov 13 15:43:13 2006 +0100
+++ b/src/Pure/General/output.ML	Mon Nov 13 15:43:14 2006 +0100
@@ -24,6 +24,7 @@
   val priority: string -> unit
   val tracing: string -> unit
   val warning: string -> unit
+  val change_warn: ('b -> 'a -> bool) -> ('a -> 'b -> 'b) -> ('a -> string) -> 'a -> 'b -> 'b
   val update_warn: ('a * 'a -> bool) -> string -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list
   val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
   val show_debug_msgs: bool ref
@@ -152,6 +153,12 @@
 fun ML_errors f = setmp do_toplevel_errors true (toplevel_errors f);
 
 
+(* overwriting change with warning *)
+
+fun change_warn ex upd msg x xs =
+  (if ex xs x then warning (msg x) else (); upd x xs);
+
+
 (* AList operations *)
 
 fun overwrite (al, p as (key, _)) =