--- a/src/HOL/Probability/Levy.thy Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Probability/Levy.thy Thu Aug 17 14:52:56 2017 +0200
@@ -500,7 +500,7 @@
show ?thesis
proof (rule tight_subseq_weak_converge [OF real_distr_M real_distr_M' tight])
fix s \<nu>
- assume s: "subseq s"
+ assume s: "strict_mono (s :: nat \<Rightarrow> nat)"
assume nu: "weak_conv_m (M \<circ> s) \<nu>"
assume *: "real_distribution \<nu>"
have 2: "\<And>n. real_distribution ((M \<circ> s) n)" unfolding comp_def by (rule assms)