1.1 --- a/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:17 2012 +0200
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:18 2012 +0200
     1.3 @@ -1035,7 +1035,7 @@
     1.4      fix X assume "X \<in> ?E"
     1.5      then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto
     1.6      then have "emeasure ?P X = emeasure M1 A * emeasure M2 B"
     1.7 -       by (simp add: emeasure_pair_measure_Times)
     1.8 +       by (simp add: M2.emeasure_pair_measure_Times)
     1.9      also have "\<dots> = emeasure M (A \<times> B)"
    1.10        using A B emeasure by auto
    1.11      finally show "emeasure ?P X = emeasure M X"
    1.12 @@ -1143,7 +1143,7 @@
    1.13        also have "\<dots> = emeasure (?S \<Otimes>\<^isub>M ?T) (A \<times> B)"
    1.14          unfolding `?S \<Otimes>\<^isub>M ?T = ?J` ..
    1.15        also have "\<dots> = emeasure ?S A * emeasure ?T B"
    1.16 -        using ab by (simp add: XY.emeasure_pair_measure_Times)
    1.17 +        using ab by (simp add: Y.emeasure_pair_measure_Times)
    1.18        finally show "prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)) =
    1.19          prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)"
    1.20          using rvs ab by (simp add: emeasure_eq_measure emeasure_distr)