diff -r 6d513469f9b2 -r 352c73a689da src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -133,7 +133,7 @@
 locale pair_subprob_space = 
   pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2
 
-sublocale pair_subprob_space \<subseteq> P: subprob_space "M1 \<Otimes>\<^sub>M M2"
+sublocale pair_subprob_space \<subseteq> P?: subprob_space "M1 \<Otimes>\<^sub>M M2"
 proof
   have "\<And>a b. \<lbrakk>a \<ge> 0; b \<ge> 0; a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a * b \<le> (1::ereal)"
     by (metis monoid_mult_class.mult.left_neutral dual_order.trans ereal_mult_right_mono)