diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Probability/Information.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -273,7 +273,13 @@
 proof -
   interpret N: prob_space N by fact
   have "finite_measure N" by unfold_locales
-  from real_RN_deriv[OF this ac] guess D . note D = this
+  from real_RN_deriv[OF this ac] obtain D
+    where D:
+      "random_variable borel D"
+      "AE x in M. RN_deriv M N x = ennreal (D x)"
+      "AE x in N. 0 < D x"
+      "\<And>x. 0 \<le> D x"
+    by this auto
 
   have "N = density M (RN_deriv M N)"
     using ac by (rule density_RN_deriv[symmetric])