diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Public.thy	Sun May 18 14:33:01 2025 +0000
@@ -407,8 +407,8 @@
 
 val analz_image_freshK_ss =
   simpset_of
-   (\<^context> delsimps [image_insert, image_Un]
-    delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
+   (\<^context> delsimps @{thms image_insert image_Un}
+    delsimps @{thms imp_disjL}    (*reduces blow-up*)
     addsimps @{thms analz_image_freshK_simps})
 
 (*Tactic for possibility theorems*)
@@ -433,7 +433,7 @@
 method_setup analz_freshK = \<open>
     Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
-      (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
+      (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}),
           REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
           ALLGOALS (asm_simp_tac (put_simpset Public.analz_image_freshK_ss ctxt))])))\<close>
     "for proving the Session Key Compromise theorem"