--- a/src/HOL/Analysis/Cross3.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Cross3.thy Thu Jul 08 08:42:36 2021 +0200
@@ -141,7 +141,7 @@
using norm_cross [of x y] by (auto simp: power_mult_distrib)
also have "... \<longleftrightarrow> \<bar>x \<bullet> y\<bar> = norm x * norm y"
using power2_eq_iff
- by (metis (mono_tags, hide_lams) abs_minus abs_norm_cancel abs_power2 norm_mult power_abs real_norm_def)
+ by (metis (mono_tags, opaque_lifting) abs_minus abs_norm_cancel abs_power2 norm_mult power_abs real_norm_def)
also have "... \<longleftrightarrow> collinear {0, x, y}"
by (rule norm_cauchy_schwarz_equal)
finally show ?thesis .