diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Library/Interval.thy
--- a/src/HOL/Library/Interval.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/Interval.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -649,7 +649,7 @@
   "0 \<le> max (la * lb) (max (la * ub) (max (lb * ua) (ua * ub)))"
   if "la \<le> 0" "0 \<le> ua"
   for la lb ua ub:: "'a::linordered_idom"
-  subgoal by (metis (no_types, hide_lams) that eq_iff min_le_iff_disj mult_zero_left mult_zero_right
+  subgoal by (metis (no_types, opaque_lifting) that eq_iff min_le_iff_disj mult_zero_left mult_zero_right
         zero_le_mult_iff)
   subgoal by (metis that le_max_iff_disj mult_zero_right order_refl zero_le_mult_iff)
   done