--- a/src/HOL/Algebra/Subrings.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Algebra/Subrings.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -357,7 +357,7 @@
     using k' A(3) subring_props(6) by auto
   thus "a \<in> K"
     using m_assoc[of "inv k" k a] A(2) inv_k subring_props(1)
-    by (metis (no_types, hide_lams) A(1) Diff_iff l_one subsetCE)
+    by (metis (no_types, opaque_lifting) A(1) Diff_iff l_one subsetCE)
 qed
 
 lemma (in ring) subfield_iff: