diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Algebra/Group.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -1120,7 +1120,7 @@
     have "(\<phi> \<one>) \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = (\<phi> \<one>) \<otimes>\<^bsub>H\<^esub> (\<phi> \<one>)"
       by (metis assms(2) image_eqI monoid.r_one one_closed phi_hom r_one surj(1))
     thus ?thesis
-      by (metis (no_types, hide_lams) Units_eq Units_one_closed assms(2) f_inv_into_f imageI
+      by (metis (no_types, opaque_lifting) Units_eq Units_one_closed assms(2) f_inv_into_f imageI
           monoid.l_one monoid.one_closed phi_hom psi_def r_one surj)
   qed