src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML

   type float = Float.float
   val approx_value : int -> (float -> float) -> string -> term * term
   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
   
   val v_elem_at : vector -> int -> string option
   val m_elem_at : matrix -> int -> vector option

 fun approx_vector prec pprt vector =
   let
     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;
   in
     pairself (HOLogic.mk_list spvecT) (Inttab.fold app vector ([], []))

 fun approx_matrix prec pprt vector =
   let
     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;
   in
     pairself (HOLogic.mk_list spmatT) (Inttab.fold app vector ([], []))