diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -398,7 +398,7 @@
 lemma has_field_derivative_higher_deriv:
      "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk>
       \<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)"
-by (metis (no_types, hide_lams) DERIV_deriv_iff_field_differentiable at_within_open comp_apply
+by (metis (no_types, opaque_lifting) DERIV_deriv_iff_field_differentiable at_within_open comp_apply
          funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def)
 
 lemma valid_path_compose_holomorphic: