src/HOL/Matrix/cplex/fspmlp.ML
changeset 23261 85f27f79232f
parent 22964 2284e0d02e7f
child 23297 06f108974fa1
--- a/src/HOL/Matrix/cplex/fspmlp.ML	Tue Jun 05 18:36:10 2007 +0200
+++ b/src/HOL/Matrix/cplex/fspmlp.ML	Tue Jun 05 19:19:30 2007 +0200
@@ -207,8 +207,8 @@
 
         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
 
@@ -288,7 +288,7 @@
                     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