# HG changeset patch
# User wenzelm
# Date 1294669817 -3600
# Node ID 0f1e411a14481071897adad8fbb24291a11ecaea
# Parent  8e2b8649507d6ab13a673fc9555e4535bdd6f604
eliminated obsolete LargeInt -- Int is unbounded;

diff -r 8e2b8649507d -r 0f1e411a1448 src/HOL/Import/shuffler.ML
--- 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')
diff -r 8e2b8649507d -r 0f1e411a1448 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- 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
 
diff -r 8e2b8649507d -r 0f1e411a1448 src/HOL/Matrix/Compute_Oracle/am_ghc.ML
--- 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])));
diff -r 8e2b8649507d -r 0f1e411a1448 src/HOL/Matrix/Compute_Oracle/am_sml.ML
--- 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
 
 
diff -r 8e2b8649507d -r 0f1e411a1448 src/HOL/Matrix/Cplex_tools.ML
--- 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")