--- a/src/HOL/Probability/Information.thy Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Probability/Information.thy Sat Mar 15 08:31:33 2014 +0100
@@ -1640,7 +1640,7 @@
using XY unfolding simple_distributed_def by auto
from finite_imageI[OF this, of fst]
have [simp]: "finite (X`space M)"
- by (simp add: image_compose[symmetric] comp_def)
+ by (simp add: image_comp comp_def)
note Y[THEN simple_distributed_finite, simp]
show "sigma_finite_measure (count_space (X ` space M))"
by (simp add: sigma_finite_measure_count_space_finite)