diff -r 662f286492b1 -r 05e2cab9af8b src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML	Tue Dec 29 16:42:01 2020 +0100
+++ b/src/Pure/General/integer.ML	Fri Jan 01 17:08:51 2021 +0100
@@ -16,6 +16,7 @@
   val div_mod: int -> int -> int * int
   val square: int -> int
   val pow: int -> int -> int (* exponent -> base -> result *)
+  val log2: int -> int
   val gcd: int -> int -> int
   val lcm: int -> int -> int
   val gcds: int list -> int
@@ -44,6 +45,8 @@
 
 fun pow k l = IntInf.pow (l, k);
 
+val log2 = IntInf.log2;
+
 fun gcd x y = PolyML.IntInf.gcd (x, y);
 fun lcm x y = abs (PolyML.IntInf.lcm (x, y));