diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Probability/Stream_Space.thy
--- a/src/HOL/Probability/Stream_Space.thy	Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Probability/Stream_Space.thy	Tue May 17 14:10:14 2022 +0100
@@ -493,7 +493,7 @@
     proof (safe intro!: sets_Sup_in_sets del: subsetI equalityI)
       fix i :: nat
       show "space (?V i) = space ?R"
-        using scylinder_streams by (subst space_measure_of) (auto simp: )
+        using scylinder_streams by (subst space_measure_of) auto
       { fix A assume "A \<in> G"
         then have "scylinder (space S) (replicate i (space S) @ [A]) = (\<lambda>s. s !! i) -` A \<inter> streams (space S)"
           by (induction i) (auto simp add: streams_shd streams_stl cong: conj_cong)