--- a/src/HOL/Probability/Probability_Measure.thy Wed Oct 10 12:12:17 2012 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Wed Oct 10 12:12:18 2012 +0200
@@ -407,7 +407,7 @@
sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^isub>M M2"
proof
show "emeasure (M1 \<Otimes>\<^isub>M M2) (space (M1 \<Otimes>\<^isub>M M2)) = 1"
- by (simp add: emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
+ by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
qed
locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +