--- a/src/HOL/Auth/Public.thy Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Auth/Public.thy Tue Feb 10 14:48:26 2015 +0100
@@ -417,7 +417,7 @@
(ALLGOALS (simp_tac (ctxt setSolver safe_solver delsimps [@{thm used_Says}]))
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*)
@@ -425,7 +425,7 @@
REPEAT
(ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
THEN
- REPEAT_FIRST (resolve_tac [refl, conjI]))
+ REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
end
*}
@@ -433,7 +433,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 Public.analz_image_freshK_ss ctxt))]))) *}
"for proving the Session Key Compromise theorem"