# HG changeset patch
# User haftmann
# Date 1127291639 -7200
# Node ID 6a52083b71c331ee7c5277fda10d0bc5900c17c1
# Parent  f662416aa5f2290a12f3e0583dac5fb6f7084e82
introduced AList module

diff -r f662416aa5f2 -r 6a52083b71c3 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Wed Sep 21 10:32:24 2005 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Wed Sep 21 10:33:59 2005 +0200
@@ -358,7 +358,7 @@
 	(* string * solver -> unit *)
 
 	fun add_solver (name, new_solver) =
-		(solvers := overwrite_warn (!solvers, (name, new_solver)) ("SAT solver " ^ quote name ^ " was defined before"));
+		(solvers := update_warn (op =) ("SAT solver " ^ quote name ^ " was defined before") (name, new_solver) (!solvers));
 
 (* ------------------------------------------------------------------------- *)
 (* invoke_solver: returns the solver associated with the given 'name'        *)
@@ -369,7 +369,7 @@
 	(* string -> solver *)
 
 	fun invoke_solver name =
-		(valOf o assoc) (!solvers, name);
+		(the o AList.lookup (op =) (!solvers)) name;
 
 end;  (* SatSolver *)