--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Thu Jul 08 08:42:36 2021 +0200
@@ -349,7 +349,7 @@
proof (rule pairwise_mono)
show "negligible (BOX (\<eta> x) x \<inter> BOX (\<eta> y) y)"
if "negligible (BOX2 (\<eta> x) x \<inter> BOX2 (\<eta> y) y)" for x y
- by (metis (no_types, hide_lams) that Int_mono negligible_subset BOX_sub)
+ by (metis (no_types, opaque_lifting) that Int_mono negligible_subset BOX_sub)
qed auto
have eq: "\<And>box. (\<lambda>D. box (\<eta> (tag D)) (tag D)) ` \<G> = (\<lambda>t. box (\<eta> t) t) ` tag ` \<G>"