--- 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