diff -r 25f28f9c28a3 -r 06f108974fa1 src/Tools/float.ML
--- a/src/Tools/float.ML	Fri Jun 08 18:13:58 2007 +0200
+++ b/src/Tools/float.ML	Sat Jun 09 00:28:46 2007 +0200
@@ -27,7 +27,7 @@
 
 type float = integer * integer;
 
-val zero = (Integer.zero, Integer.zero);
+val zero: float = (0, 0);
 
 fun add (a1, b1) (a2, b2) =
   if Integer.cmp (b1, b2) = LESS then
@@ -54,7 +54,7 @@
 fun min r s = case cmp (r, s) of LESS => r | _ => s;
 fun max r s = case cmp (r, s) of LESS => s | _ => r;
 
-fun positive_part (a, b) = (Integer.max Integer.zero a, b);
-fun negative_part (a, b) = (Integer.min Integer.zero a, b);
+fun positive_part (a, b) = (Integer.max 0 a, b);
+fun negative_part (a, b) = (Integer.min 0 a, b);
 
 end;