--- a/src/HOL/Matrix_LP/float_arith.ML	Tue Dec 29 16:42:01 2020 +0100
+++ b/src/HOL/Matrix_LP/float_arith.ML	Fri Jan 01 17:08:51 2021 +0100
@@ -105,7 +105,7 @@
       else
         (exp5 (~ d), d)
 
-    val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10)
+    val L = Real.floor (int2real (Integer.log2 q) + int2real r * ln2_10)
     val L1 = L + 1
 
     val (q1, r1) = subtract (q, r) (bin2dec L1)