diff -r 40a1865ab122 -r c3d1590debd8 doc-src/TutorialI/Protocol/Public.thy
--- a/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 20 11:26:59 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 20 15:24:18 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Auth/Public
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
@@ -153,15 +152,15 @@
 
 (*Tactic for possibility theorems*)
 ML {*
-fun possibility_tac st = st |>
+fun possibility ctxt =
     REPEAT (*omit used_Says so that Nonces start from different traces!*)
-    (ALLGOALS (simp_tac (@{simpset} delsimps [used_Says]))
+    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says]))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac [refl, conjI, @{thm Nonce_supply}]));
 *}
 
-method_setup possibility = {* Scan.succeed (K (SIMPLE_METHOD possibility_tac)) *}
+method_setup possibility = {* Scan.succeed (SIMPLE_METHOD o possibility_tac) *}
     "for proving possibility theorems"
 
 end