diff -r 833d154ab189 -r 0fa87bd86566 src/Tools/float.ML
--- a/src/Tools/float.ML	Thu Feb 01 13:55:10 2018 +0100
+++ b/src/Tools/float.ML	Thu Feb 01 15:12:57 2018 +0100
@@ -48,7 +48,7 @@
 
 fun ord (r, s) = sign (sub r s);
 
-fun eq (r, s) = ord (r, s) = EQUAL;
+val eq = is_equal o ord;
 
 fun min r s = case ord (r, s) of LESS => r | _ => s;
 fun max r s = case ord (r, s) of LESS => s | _ => r;