SML/NJ compatibility fixes
authorwebertj
Thu Mar 11 00:15:24 2004 +0100 (2004-03-11)
changeset 1446004e787a4f17a
parent 14459 0a8619367a61
child 14461 fab539f843d9
SML/NJ compatibility fixes
src/HOL/Tools/refute.ML
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Wed Mar 10 22:39:12 2004 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Mar 11 00:15:24 2004 +0100
     1.3 @@ -686,7 +686,7 @@
     1.4  
     1.5  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
     1.6  
     1.7 -	fun boundvar_interpreter thy model args (Bound i) = Some (nth_elem (i, #bounds args), model, args)
     1.8 +	fun boundvar_interpreter thy model args (Bound i) = Some (nth_elem (i, #bounds (args:arguments)), model, args)
     1.9  	  | boundvar_interpreter thy model args _         = None;
    1.10  
    1.11  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
     2.1 --- a/src/HOL/Tools/sat_solver.ML	Wed Mar 10 22:39:12 2004 +0100
     2.2 +++ b/src/HOL/Tools/sat_solver.ML	Thu Mar 11 00:15:24 2004 +0100
     2.3 @@ -198,7 +198,7 @@
     2.4  (* solvers: a (reference to a) table of all registered SAT solvers           *)
     2.5  (* ------------------------------------------------------------------------- *)
     2.6  
     2.7 -	val solvers = ref Symtab.empty;
     2.8 +	val solvers = ref (Symtab.empty : solver Symtab.table);
     2.9  
    2.10  (* ------------------------------------------------------------------------- *)
    2.11  (* add_solver: updates 'solvers' by adding a new solver                      *)
    2.12 @@ -209,7 +209,7 @@
    2.13  	(* string * solver -> unit *)
    2.14  
    2.15  	fun add_solver (name, new_solver) =
    2.16 -		solvers := Symtab.update_new ((name, new_solver), !solvers);
    2.17 +		(solvers := Symtab.update_new ((name, new_solver), !solvers));
    2.18  
    2.19  (* ------------------------------------------------------------------------- *)
    2.20  (* invoke_solver: returns the solver associated with the given 'name'        *)