src/HOL/SET_Protocol/Public_SET.thy

 fun possibility_tac ctxt =
     REPEAT (*omit used_Says so that Nonces start from different traces!*)
     (ALLGOALS (simp_tac (ctxt delsimps [@{thm used_Says}, @{thm used_Notes}]))
      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 SET_CR!), where we have to set up some
   nonces and keys initially*)
 fun basic_possibility_tac ctxt =
     REPEAT 
     (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
      THEN
-     REPEAT_FIRST (resolve_tac [refl, conjI]))
+     REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
 *}
 
 method_setup possibility = {*
     Scan.succeed (SIMPLE_METHOD o possibility_tac) *}
     "for proving possibility theorems"