src/HOL/Matrix/cplex/fspmlp.ML

         fun isnegstr x = String.isPrefix "-" x
         fun negstr x = if isnegstr x then String.extract (x, 1, NONE) else "-"^x
 
         fun test_1 (lower, upper) =
             if lower = upper then
-                (if Float.eq (lower, (Intt.int ~1, Intt.zero)) then ~1
-                 else if Float.eq (lower, (Intt.int 1, Intt.zero)) then 1
+                (if Float.eq (lower, (Integer.int ~1, Integer.zero)) then ~1
+                 else if Float.eq (lower, (Integer.int 1, Integer.zero)) then 1
                  else 0)
             else 0
 
         fun calcr (row_index, a) g =
             let

                     val index = xlen-i
                     val (r, (r12_1, r12_2)) = abs_estimate (i-1) r1 r2
                     val b1 = case Inttab.lookup r1 index of NONE => raise (Load ("x-value not bounded from below: "^(names index))) | SOME x => x
                     val b2 = case Inttab.lookup r2 index of NONE => raise (Load ("x-value not bounded from above: "^(names index))) | SOME x => x
                     val abs_max = Float.max (Float.neg (Float.negative_part b1)) (Float.positive_part b2)
-                    val i' = Intt.int index
+                    val i' = Integer.int index
                 in
                     (add_row_entry r i' abs_max, (add_row_entry r12_1 i' b1, add_row_entry r12_2 i' b2))
                 end
         val (r, (r1, r2)) = abs_estimate xlen r1 r2
     in