--- a/src/HOL/Auth/Smartcard/Smartcard.thy Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Tue Feb 10 14:48:26 2015 +0100
@@ -374,7 +374,7 @@
setSolver safe_solver))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
- resolve_tac [refl, conjI, @{thm Nonce_supply}])))
+ resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}])))
(*For harder protocols (such as Recur) where we have to set up some
nonces and keys initially*)
@@ -382,7 +382,7 @@
REPEAT
(ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
THEN
- REPEAT_FIRST (resolve_tac [refl, conjI]))
+ REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
val analz_image_freshK_ss =
simpset_of
@@ -403,7 +403,7 @@
method_setup analz_freshK = {*
Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
- (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
+ (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt))]))) *}
"for proving the Session Key Compromise theorem"