src/HOL/Tools/sat_solver.ML
changeset 22220 6dc8d0dca678
parent 21858 05f57309170c
child 22567 1565d476a9e2
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Wed Jan 31 16:05:12 2007 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Wed Jan 31 16:05:13 2007 +0100
     1.3 @@ -357,8 +357,13 @@
     1.4  
     1.5  	(* string * solver -> unit *)
     1.6  
     1.7 -	fun add_solver (name, new_solver) =
     1.8 -		(solvers := update_warn (op =) ("SAT solver " ^ quote name ^ " was defined before") (name, new_solver) (!solvers));
     1.9 +    fun add_solver (name, new_solver) =
    1.10 +      let
    1.11 +        val the_solvers = !solvers;
    1.12 +        val _ = if AList.defined (op =) the_solvers name
    1.13 +          then warning ("SAT solver " ^ quote name ^ " was defined before")
    1.14 +          else ();
    1.15 +      in solvers := AList.update (op =) (name, new_solver) the_solvers end;
    1.16  
    1.17  (* ------------------------------------------------------------------------- *)
    1.18  (* invoke_solver: returns the solver associated with the given 'name'        *)