diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Auth/Smartcard/Smartcard.thy
--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Sun May 18 14:33:01 2025 +0000
@@ -383,8 +383,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})
 end
 \<close>
@@ -400,7 +400,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 Smartcard.analz_image_freshK_ss ctxt))])))\<close>
     "for proving the Session Key Compromise theorem"