--- a/src/HOL/Import/shuffler.ML Mon Jan 10 15:19:48 2011 +0100
+++ b/src/HOL/Import/shuffler.ML Mon Jan 10 15:30:17 2011 +0100
@@ -465,7 +465,7 @@
end
| F (Abs(x,xT,t),idx) =
let
- val x' = "x" ^ (LargeInt.toString idx) (* amazing *)
+ val x' = "x" ^ Int.toString idx
val (t',idx') = F (t,idx+1)
in
(Abs(x',xT,t'),idx')
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Mon Jan 10 15:19:48 2011 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Mon Jan 10 15:30:17 2011 +0100
@@ -584,7 +584,7 @@
fun maximal_element fld amat acc =
fld (fn (m,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc
fun float_of_rat x = let val (a,b) = Rat.quotient_of_rat x
- in Real.fromLargeInt a / Real.fromLargeInt b end;
+ in Real.fromInt a / Real.fromInt b end;
in
fun pi_scale_then solver (obj:vector) mats =
@@ -616,7 +616,7 @@
fun maximal_element fld amat acc =
fld (fn (m,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc
fun float_of_rat x = let val (a,b) = Rat.quotient_of_rat x
- in Real.fromLargeInt a / Real.fromLargeInt b end;
+ in Real.fromInt a / Real.fromInt b end;
fun int_of_float x = (trunc x handle Overflow => 0 | Domain => 0)
in
--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Mon Jan 10 15:19:48 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Mon Jan 10 15:30:17 2011 +0100
@@ -206,7 +206,7 @@
val c = !guid_counter
val _ = guid_counter := !guid_counter + 1
in
- (LargeInt.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c)
+ (Int.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c)
end
fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
--- a/src/HOL/Matrix/Compute_Oracle/am_sml.ML Mon Jan 10 15:19:48 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_sml.ML Mon Jan 10 15:30:17 2011 +0100
@@ -486,7 +486,7 @@
val c = !guid_counter
val _ = guid_counter := !guid_counter + 1
in
- (LargeInt.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c)
+ (Int.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c)
end
--- a/src/HOL/Matrix/Cplex_tools.ML Mon Jan 10 15:19:48 2011 +0100
+++ b/src/HOL/Matrix/Cplex_tools.ML Mon Jan 10 15:30:17 2011 +0100
@@ -1134,7 +1134,7 @@
fun solve_glpk prog =
let
- val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))
+ val name = Int.toString (Time.toMicroseconds (Time.now ()))
val lpname = tmp_file (name^".lp")
val resultname = tmp_file (name^".txt")
val _ = save_cplexFile lpname prog
@@ -1165,7 +1165,7 @@
()
end
- val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))
+ val name = Int.toString (Time.toMicroseconds (Time.now ()))
val lpname = tmp_file (name^".lp")
val resultname = tmp_file (name^".txt")
val scriptname = tmp_file (name^".script")