diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -347,7 +347,7 @@
 lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_inv:
   "orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
   for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
-  by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
+  by (metis (no_types, opaque_lifting) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
 
 lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_norm:
   "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"