# HG changeset patch
# User obua
# Date 1094644551 -7200
# Node ID 9cfbc392918ca3aa58664e7b60f71eafe9ac3c64
# Parent  9d57263faf9edb2867fbc41fb1cd7dc73492d7d8
Adapted FloatArith.ML to SMLNJ 10.0.7

diff -r 9d57263faf9e -r 9cfbc392918c src/HOL/Matrix/FloatArith.ML
--- a/src/HOL/Matrix/FloatArith.ML	Tue Sep 07 16:02:42 2004 +0200
+++ b/src/HOL/Matrix/FloatArith.ML	Wed Sep 08 13:55:51 2004 +0200
@@ -28,13 +28,13 @@
 fun ipow2 a = IntInf.pow ((IntInf.fromInt 2), IntInf.toInt a)
 
 fun add (a1, b1) (a2, b2) = 
-    if b1 < b2 then
+    if IntInf.< (b1, b2) then
 	(iadd a1 (imul a2 (ipow2 (isub b2 b1))), b1)
     else
 	(iadd (imul a1 (ipow2 (isub b1 b2))) a2, b2)
 
 fun sub (a1, b1) (a2, b2) = 
-    if b1 < b2 then
+    if IntInf.< (b1, b2) then
 	(isub a1 (imul a2 (ipow2 (isub b2 b1))), b1)
     else
 	(isub (imul a1 (ipow2 (isub b1 b2))) a2, b2)