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