diff -r f164526d8727 -r 158ab2239496 src/HOL/Probability/Stream_Space.thy
--- a/src/HOL/Probability/Stream_Space.thy	Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/Stream_Space.thy	Thu Jun 16 23:03:27 2016 +0200
@@ -94,16 +94,16 @@
   shows "(\<lambda>x. f x ## g x) \<in> measurable N (stream_space M)"
   by (rule measurable_stream_space2) (simp add: Stream_snth)
 
-lemma measurable_smap[measurable]: 
+lemma measurable_smap[measurable]:
   assumes X[measurable]: "X \<in> measurable N M"
   shows "smap X \<in> measurable (stream_space N) (stream_space M)"
   by (rule measurable_stream_space2) simp
 
-lemma measurable_stake[measurable]: 
+lemma measurable_stake[measurable]:
   "stake i \<in> measurable (stream_space (count_space UNIV)) (count_space (UNIV :: 'a::countable list set))"
   by (induct i) auto
 
-lemma measurable_shift[measurable]: 
+lemma measurable_shift[measurable]:
   assumes f: "f \<in> measurable N (stream_space M)"
   assumes [measurable]: "g \<in> measurable N (stream_space M)"
   shows "(\<lambda>x. stake n (f x) @- g x) \<in> measurable N (stream_space M)"
@@ -168,7 +168,7 @@
 lemma (in prob_space) nn_integral_stream_space:
   assumes [measurable]: "f \<in> borel_measurable (stream_space M)"
   shows "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+x. (\<integral>\<^sup>+X. f (x ## X) \<partial>stream_space M) \<partial>M)"
-proof -                  
+proof -
   interpret S: sequence_space M ..
   interpret P: pair_sigma_finite M "\<Pi>\<^sub>M i::nat\<in>UNIV. M" ..
 
@@ -230,7 +230,7 @@
     apply (simp add: AE_iff_nn_integral[symmetric])
     done
 qed
-  
+
 lemma (in prob_space) AE_stream_all:
   assumes [measurable]: "Measurable.pred M P" and P: "AE x in M. P x"
   shows "AE x in stream_space M. stream_all P x"
@@ -271,14 +271,14 @@
   assumes sets: "\<And>i. (\<lambda>x. x !! i) \<in> measurable N M"
   shows "sets (stream_space M) \<subseteq> sets N"
   unfolding stream_space_def sets_distr
-  by (auto intro!: sets_image_in_sets measurable_Sup_sigma2 measurable_vimage_algebra2 del: subsetI equalityI 
+  by (auto intro!: sets_image_in_sets measurable_Sup2 measurable_vimage_algebra2 del: subsetI equalityI
            simp add: sets_PiM_eq_proj snth_in space sets cong: measurable_cong_sets)
 
 lemma sets_stream_space_eq: "sets (stream_space M) =
-    sets (\<Squnion>\<^sub>\<sigma> i\<in>UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)"
+    sets (SUP i:UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)"
   by (auto intro!: sets_stream_space_in_sets sets_Sup_in_sets sets_image_in_sets
-                   measurable_Sup_sigma1  snth_in measurable_vimage_algebra1 del: subsetI
-           simp: space_Sup_sigma space_stream_space)
+                   measurable_Sup1 snth_in measurable_vimage_algebra1 del: subsetI
+           simp: space_Sup_eq_UN space_stream_space)
 
 lemma sets_restrict_stream_space:
   assumes S[measurable]: "S \<in> sets M"
@@ -288,17 +288,17 @@
   apply (simp add: space_stream_space streams_mono2)
   apply (subst vimage_algebra_cong[OF refl refl sets_stream_space_eq])
   apply (subst sets_stream_space_eq)
-  apply (subst sets_vimage_Sup_eq)
+  apply (subst sets_vimage_Sup_eq[where Y="streams (space M)"])
   apply simp
+  apply auto []
   apply (auto intro: streams_mono) []
+  apply auto []
   apply (simp add: image_image space_restrict_space)
-  apply (intro SUP_sigma_cong)
   apply (simp add: vimage_algebra_cong[OF refl refl restrict_space_eq_vimage_algebra])
   apply (subst (1 2) vimage_algebra_vimage_algebra_eq)
-  apply (auto simp: streams_mono snth_in)
+  apply (auto simp: streams_mono snth_in )
   done
 
-
 primrec sstart :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a stream set" where
   "sstart S [] = streams S"
 | [simp del]: "sstart S (x # xs) = op ## x ` sstart S xs"