diff -r 970964690b3d -r 199d1d5bb17e src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:18 2012 +0200
@@ -194,7 +194,7 @@
   unfolding KL_divergence_def
 proof (subst integral_density)
   show "entropy_density b M (density M (\<lambda>x. ereal (f x))) \<in> borel_measurable M"
-    using f `1 < b`
+    using f
     by (auto simp: comp_def entropy_density_def intro!: borel_measurable_log borel_measurable_RN_deriv_density)
   have "density M (RN_deriv M (density M f)) = density M f"
     using f by (intro density_RN_deriv_density) auto