--- 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)