diff -r 6d513469f9b2 -r 352c73a689da src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -461,7 +461,7 @@
 
 locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2
 
-sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^sub>M M2"
+sublocale pair_prob_space \<subseteq> P?: prob_space "M1 \<Otimes>\<^sub>M M2"
 proof
   show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) = 1"
     by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
@@ -471,7 +471,7 @@
   fixes I :: "'i set"
   assumes prob_space: "\<And>i. prob_space (M i)"
 
-sublocale product_prob_space \<subseteq> M: prob_space "M i" for i
+sublocale product_prob_space \<subseteq> M?: prob_space "M i" for i
   by (rule prob_space)
 
 locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I