--- a/src/HOL/Analysis/Riemann_Mapping.thy Thu Jul 11 18:37:52 2019 +0200
+++ b/src/HOL/Analysis/Riemann_Mapping.thy Wed Jul 17 14:02:42 2019 +0100
@@ -576,7 +576,7 @@
(contour_integral (?g z) f - (contour_integral (?g x) f + f x * (z - x))) -
(contour_integral (linepath x z) f - f x * (z - x)) /\<^sub>R norm (z - x))
\<midarrow>x\<rightarrow> 0"
- apply (rule Lim_eventually)
+ apply (rule tendsto_eventually)
apply (simp add: eventually_at)
apply (rule_tac x=d in exI)
using \<open>d > 0\<close> * by simp