diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Cartesian_Space.thy
--- a/src/HOL/Analysis/Cartesian_Space.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -1158,7 +1158,7 @@
   "orthogonal_transformation f \<longleftrightarrow> f(0::'a::real_inner) = (0::'a) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
   unfolding orthogonal_transformation
   apply (auto simp: linear_0 isometry_linear)
-   apply (metis (no_types, hide_lams) dist_norm linear_diff)
+   apply (metis (no_types, opaque_lifting) dist_norm linear_diff)
   by (metis dist_0_norm)