--- a/src/HOL/SET_Protocol/Public_SET.thy Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/SET_Protocol/Public_SET.thy Tue Feb 10 14:48:26 2015 +0100
@@ -347,7 +347,7 @@
(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*)
@@ -355,7 +355,7 @@
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 = {*