diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Complex_Analysis/Complex_Singularities.thy
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -542,7 +542,7 @@
         using that by (auto intro!:tendsto_eq_intros)
       then have "fg \<midarrow>z\<rightarrow> 0"
         apply (elim Lim_transform_within[OF _ \<open>r1>0\<close>])
-        by (metis (no_types, hide_lams) Diff_iff cball_trivial dist_commute dist_self
+        by (metis (no_types, opaque_lifting) Diff_iff cball_trivial dist_commute dist_self
               eq_iff_diff_eq_0 fg_times less_le linorder_not_le mem_ball mem_cball powr_of_int
               that)
       then show ?thesis unfolding not_essential_def fg_def by auto