diff -r 0c5cd369a643 -r 50b60f501b05 src/HOL/Auth/Public.thy
--- 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"