src/HOL/Tools/sat_solver.ML
changeset 22220 6dc8d0dca678
parent 21858 05f57309170c
child 22567 1565d476a9e2
--- 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'        *)