diff -r 7d59af98af29 -r 2a4c8a2a3f8e src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Wed Dec 26 20:57:23 2018 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Dec 27 19:48:28 2018 +0100
@@ -212,7 +212,7 @@
 
 lemma real_lim:
   fixes l::complex
-  assumes "(f \<longlongrightarrow> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
+  assumes "(f \<longlongrightarrow> l) F" and "\<not> trivial_limit F" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
   shows  "l \<in> \<real>"
 proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)])
   show "eventually (\<lambda>x. f x \<in> \<real>) F"