diff --git a/doc/next-release.md b/doc/next-release.md
index 3c8c5237d7..b136fdefb3 100644
--- a/doc/next-release.md
+++ b/doc/next-release.md
@@ -200,6 +200,8 @@ Incompatibilities:
     `suminf_def` to reflect its overloading to `suminf`. (All these definitions
     are generalized versions of those in `seqTheory`.)
 
+*   The constant `lg` (logarithm with base 2) has moved from the `util_prob` theory to `transc`.
+
 * * * * *
 
 <div class="footer">
diff --git a/examples/computability/kolmog/kraft_ineqScript.sml b/examples/computability/kolmog/kraft_ineqScript.sml
index 25b9316efa..90ad731fbf 100644
--- a/examples/computability/kolmog/kraft_ineqScript.sml
+++ b/examples/computability/kolmog/kraft_ineqScript.sml
@@ -20,6 +20,8 @@ val _ = new_theory "kraft_ineq";
 
 val _ = intLib.deprecate_int()
 
+val _ = hide "lg" (* transc$lg is now log base 2 *)
+
 Theorem bool_list_card[simp]:
   CARD {s | LENGTH (s:bool list) = n} = 2**n
 Proof