src/HOL/Auth/Shared.thy

 
 method_setup analz_freshK = {*
     Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
-          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
+          REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
           ALLGOALS (asm_simp_tac (put_simpset Shared.analz_image_freshK_ss ctxt))]))) *}
     "for proving the Session Key Compromise theorem"
 
 method_setup possibility = {*
     Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}