# HG changeset patch
# User webertj
# Date 1078960524 -3600
# Node ID 04e787a4f17a16fe1705917c735573a160af7c16
# Parent  0a8619367a6101fbc4585c81287ee81ffa66616d
SML/NJ compatibility fixes

diff -r 0a8619367a61 -r 04e787a4f17a src/HOL/Tools/refute.ML
--- 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 *)
diff -r 0a8619367a61 -r 04e787a4f17a src/HOL/Tools/sat_solver.ML
--- 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'        *)