introduced AList module
authorhaftmann
Wed Sep 21 10:33:59 2005 +0200 (2005-09-21)
changeset 175416a52083b71c3
parent 17540 f662416aa5f2
child 17542 b588e06b6775
introduced AList module
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Wed Sep 21 10:32:24 2005 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Wed Sep 21 10:33:59 2005 +0200
     1.3 @@ -358,7 +358,7 @@
     1.4  	(* string * solver -> unit *)
     1.5  
     1.6  	fun add_solver (name, new_solver) =
     1.7 -		(solvers := overwrite_warn (!solvers, (name, new_solver)) ("SAT solver " ^ quote name ^ " was defined before"));
     1.8 +		(solvers := update_warn (op =) ("SAT solver " ^ quote name ^ " was defined before") (name, new_solver) (!solvers));
     1.9  
    1.10  (* ------------------------------------------------------------------------- *)
    1.11  (* invoke_solver: returns the solver associated with the given 'name'        *)
    1.12 @@ -369,7 +369,7 @@
    1.13  	(* string -> solver *)
    1.14  
    1.15  	fun invoke_solver name =
    1.16 -		(valOf o assoc) (!solvers, name);
    1.17 +		(the o AList.lookup (op =) (!solvers)) name;
    1.18  
    1.19  end;  (* SatSolver *)
    1.20