--- a/src/HOL/Tools/refute.ML Wed Mar 10 22:39:12 2004 +0100
+++ b/src/HOL/Tools/refute.ML Thu Mar 11 00:15:24 2004 +0100
@@ -686,7 +686,7 @@
(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
- fun boundvar_interpreter thy model args (Bound i) = Some (nth_elem (i, #bounds args), model, args)
+ fun boundvar_interpreter thy model args (Bound i) = Some (nth_elem (i, #bounds (args:arguments)), model, args)
| boundvar_interpreter thy model args _ = None;
(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
--- 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' *)