Fixed compatibility issues with SML/NJ:
authorwebertj
Mon Jan 12 14:35:07 2004 +0100 (2004-01-12)
changeset 14351cd3ef10d02be
parent 14350 41b32020d0b3
child 14352 a8b1a44d8264
Fixed compatibility issues with SML/NJ:
- replaced '(op *)' by 'op*'
- replaced 'LargeInt' by 'Int'
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Sat Jan 10 13:35:10 2004 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Jan 12 14:35:07 2004 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4  		val prep_ext = I;
     1.5  		val merge =
     1.6  			fn (symTable1, symTable2) =>
     1.7 -				(Symtab.merge (op =) (symTable1, symTable2));
     1.8 +				(Symtab.merge (op=) (symTable1, symTable2));
     1.9  		fun print sg symTable =
    1.10  			writeln
    1.11  				("'refute', default parameters:\n" ^
    1.12 @@ -493,7 +493,7 @@
    1.13  						None
    1.14  					(* string -> int list *)
    1.15  					fun string_to_int_list s =
    1.16 -						mapfilter (option o LargeInt.fromString) (space_explode " " s)
    1.17 +						mapfilter (option o Int.fromString) (space_explode " " s)
    1.18  					(* string -> string -> bool *)
    1.19  					fun is_substring s1 s2 =
    1.20  					let
    1.21 @@ -717,7 +717,7 @@
    1.22  
    1.23  	(* int list -> int *)
    1.24  
    1.25 -	fun sum xs = foldl (op +) (0, xs);
    1.26 +	fun sum xs = foldl op+ (0, xs);
    1.27  
    1.28  (* ------------------------------------------------------------------------- *)
    1.29  (* product: computes the product of a list of integers; product [] = 1       *)
    1.30 @@ -725,7 +725,7 @@
    1.31  
    1.32  	(* int list -> int *)
    1.33  
    1.34 -	fun product xs = foldl (op *) (1, xs);
    1.35 +	fun product xs = foldl op* (1, xs);
    1.36  
    1.37  (* ------------------------------------------------------------------------- *)
    1.38  (* power: power(a,b) computes a^b, for a>=0, b>=0                            *)
    1.39 @@ -1507,7 +1507,7 @@
    1.40  		(* (string * string) list * string -> int *)
    1.41  		fun read_int (parms, name) =
    1.42  			case assoc_string (parms, name) of
    1.43 -			  Some s => (case LargeInt.fromString s of
    1.44 +			  Some s => (case Int.fromString s of
    1.45  				  SOME i => i
    1.46  				| NONE   => error ("parameter '" ^ name ^ "' (value is '" ^ s ^ "') must be an integer value"))
    1.47  			| None   => error ("parameter '" ^ name ^ "' must be assigned a value")