src/HOL/Auth/Public.thy

--- a/src/HOL/Auth/Public.thy	Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/Auth/Public.thy	Sat Jul 18 20:54:56 2015 +0200
@@ -434,7 +434,7 @@
     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 Public.analz_image_freshK_ss ctxt))]))) *}
     "for proving the Session Key Compromise theorem"