--- a/src/HOL/Probability/Measure_Space.thy Mon Apr 20 13:46:36 2015 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Tue Apr 21 17:19:00 2015 +0100
@@ -389,7 +389,7 @@
ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
by (simp add: zero_ereal_def)
then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
- by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const])
+ by (rule Lim_transform[OF tendsto_const])
then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
using A by (subst (1 2) f') auto
qed