src/HOL/Tools/sat_solver.ML
changeset 14460 04e787a4f17a
parent 14453 3397a69dfa4e
child 14487 157d0ea7b2da
--- a/src/HOL/Tools/sat_solver.ML	Wed Mar 10 22:39:12 2004 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Thu Mar 11 00:15:24 2004 +0100
@@ -198,7 +198,7 @@
 (* solvers: a (reference to a) table of all registered SAT solvers           *)
 (* ------------------------------------------------------------------------- *)
 
-	val solvers = ref Symtab.empty;
+	val solvers = ref (Symtab.empty : solver Symtab.table);
 
 (* ------------------------------------------------------------------------- *)
 (* add_solver: updates 'solvers' by adding a new solver                      *)
@@ -209,7 +209,7 @@
 	(* string * solver -> unit *)
 
 	fun add_solver (name, new_solver) =
-		solvers := Symtab.update_new ((name, new_solver), !solvers);
+		(solvers := Symtab.update_new ((name, new_solver), !solvers));
 
 (* ------------------------------------------------------------------------- *)
 (* invoke_solver: returns the solver associated with the given 'name'        *)