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