diff -r eb6d86fb7ed3 -r 85f27f79232f src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
--- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Tue Jun 05 18:36:10 2007 +0200
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Tue Jun 05 19:19:30 2007 +0200
@@ -14,8 +14,8 @@
   val approx_vector : int -> (float -> float) -> vector -> term * term
   val approx_matrix : int -> (float -> float) -> matrix -> term * term
 
-  val mk_spvec_entry : Intt.int -> float -> term
-  val mk_spmat_entry : Intt.int -> term -> term
+  val mk_spvec_entry : integer -> float -> term
+  val mk_spmat_entry : integer -> term -> term
   val spvecT: typ
   val spmatT: typ
   
@@ -64,7 +64,7 @@
     fun app (index, s) (lower, upper) =
       let
         val (flower, fupper) = approx_value prec pprt s
-        val index = HOLogic.mk_number HOLogic.natT (Intt.int index)
+        val index = HOLogic.mk_number HOLogic.natT (Integer.int index)
         val elower = HOLogic.mk_prod (index, flower)
         val eupper = HOLogic.mk_prod (index, fupper)
       in (elower :: lower, eupper :: upper) end;
@@ -77,7 +77,7 @@
     fun app (index, v) (lower, upper) =
       let
         val (flower, fupper) = approx_vector prec pprt v
-        val index = HOLogic.mk_number HOLogic.natT (Intt.int index)
+        val index = HOLogic.mk_number HOLogic.natT (Integer.int index)
         val elower = HOLogic.mk_prod (index, flower)
         val eupper = HOLogic.mk_prod (index, fupper)
       in (elower :: lower, eupper :: upper) end;