src/HOL/Auth/Message.thy

--- a/src/HOL/Auth/Message.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Auth/Message.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -214,7 +214,7 @@
 lemma parts_image [simp]:
   "parts (f ` A) = (\<Union>x\<in>A. parts {f x})"
   apply auto
-  apply (metis (mono_tags, hide_lams) image_iff parts_singleton)
+  apply (metis (mono_tags, opaque_lifting) image_iff parts_singleton)
   apply (metis empty_subsetI image_eqI insert_absorb insert_subset parts_mono)
   done