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