diff -r 6d96ee03b62e -r 4df0628e8545 src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Thu Jul 11 18:37:52 2019 +0200
+++ b/src/HOL/Probability/Distributions.thy	Wed Jul 17 14:02:42 2019 +0100
@@ -116,7 +116,7 @@
   show "?X \<longlonglongrightarrow> (\<integral>\<^sup>+x. ennreal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)"
     apply (intro nn_integral_LIMSEQ)
     apply (auto simp: incseq_def le_fun_def eventually_sequentially
-                split: split_indicator intro!: Lim_eventually)
+                split: split_indicator intro!: tendsto_eventually)
     apply (metis nat_ceiling_le_eq)
     done