diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Library/Equipollence.thy
--- a/src/HOL/Library/Equipollence.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/Equipollence.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -125,7 +125,7 @@
   show "S \<lesssim> {()}" if "S \<subseteq> {x}" for x
     using subset_imp_lepoll [OF that] by (simp add: singleton_eqpoll lepoll_trans2)
   show "\<exists>x. S \<subseteq> {x}" if "S \<lesssim> {()}"
-  by (metis (no_types, hide_lams) image_empty image_insert lepoll_iff that)
+  by (metis (no_types, opaque_lifting) image_empty image_insert lepoll_iff that)
 qed
 
 lemma infinite_insert_lepoll: