diff -r 970964690b3d -r 199d1d5bb17e src/HOL/Probability/Probability_Measure.thy
--- 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" +