1.1 --- a/src/HOL/Probability/Independent_Family.thy	Thu Aug 18 17:42:35 2011 +0200
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Thu Aug 18 13:36:58 2011 -0700
     1.3 @@ -563,7 +563,7 @@
     1.4      with F have "(\<lambda>i. prob X * prob (F i)) sums prob (X \<inter> (\<Union>i. F i))"
     1.5        by simp
     1.6      moreover have "(\<lambda>i. prob X * prob (F i)) sums (prob X * prob (\<Union>i. F i))"
     1.7 -      by (intro mult_right.sums finite_measure_UNION F dis)
     1.8 +      by (intro sums_mult finite_measure_UNION F dis)
     1.9      ultimately have "prob (X \<inter> (\<Union>i. F i)) = prob X * prob (\<Union>i. F i)"
    1.10        by (auto dest!: sums_unique)
    1.11      with F show "(\<Union>i. F i) \<in> sets ?D"