dropped Output.update_warn

--- a/src/HOL/Tools/sat_solver.ML	Wed Jan 31 16:05:12 2007 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Wed Jan 31 16:05:13 2007 +0100
@@ -357,8 +357,13 @@
 
 	(* string * solver -> unit *)
 
-	fun add_solver (name, new_solver) =
-		(solvers := update_warn (op =) ("SAT solver " ^ quote name ^ " was defined before") (name, new_solver) (!solvers));
+    fun add_solver (name, new_solver) =
+      let
+        val the_solvers = !solvers;
+        val _ = if AList.defined (op =) the_solvers name
+          then warning ("SAT solver " ^ quote name ^ " was defined before")
+          else ();
+      in solvers := AList.update (op =) (name, new_solver) the_solvers end;
 
 (* ------------------------------------------------------------------------- *)
 (* invoke_solver: returns the solver associated with the given 'name'        *)

--- a/src/Pure/General/output.ML	Wed Jan 31 16:05:12 2007 +0100
+++ b/src/Pure/General/output.ML	Wed Jan 31 16:05:13 2007 +0100
@@ -24,8 +24,6 @@
   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 debugging: bool ref
   val no_warnings: ('a -> 'b) -> 'a -> 'b
@@ -155,12 +153,6 @@
 
 (* 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, _)) =
   let fun over ((q as (keyi, _)) :: pairs) =
             if keyi = key then p :: pairs else q :: (over pairs)
@@ -171,10 +163,6 @@
  (if is_none (AList.lookup (op =) alist a) then () else warning msg;
   overwrite args);
 
-fun update_warn eq msg (kv as (key, value)) xs =
- (if (not o AList.defined eq xs) key then () else warning msg;
-  AList.update eq kv xs);
-
 
 (* add_mode *)