diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Stream_Space.thy
--- a/src/HOL/Probability/Stream_Space.thy	Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Stream_Space.thy	Mon Nov 24 12:20:14 2014 +0100
@@ -41,7 +41,8 @@
 lemma stream_space_eq_distr: "stream_space M = distr (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M) to_stream"
   unfolding stream_space_def by (rule distr_cong) auto
 
-lemma sets_stream_space_cong: "sets M = sets N \<Longrightarrow> sets (stream_space M) = sets (stream_space N)"
+lemma sets_stream_space_cong[measurable_cong]:
+  "sets M = sets N \<Longrightarrow> sets (stream_space M) = sets (stream_space N)"
   using sets_eq_imp_space_eq[of M N] by (simp add: stream_space_def vimage_algebra_def cong: sets_PiM_cong)
 
 lemma measurable_snth_PiM: "(\<lambda>\<omega> n. \<omega> !! n) \<in> measurable (stream_space M) (\<Pi>\<^sub>M i\<in>UNIV. M)"