src/Doc/Tutorial/Protocol/Public.thy

--- a/src/Doc/Tutorial/Protocol/Public.thy	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Doc/Tutorial/Protocol/Public.thy	Tue Feb 10 14:48:26 2015 +0100
@@ -162,7 +162,7 @@
     (ALLGOALS (simp_tac (ctxt delsimps [used_Says]))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
-                   resolve_tac [refl, conjI, @{thm Nonce_supply}]));
+                   resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}]));
 *}
 
 method_setup possibility = {* Scan.succeed (SIMPLE_METHOD o possibility_tac) *}