1.1 --- a/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Auth/Public
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1996  University of Cambridge
     1.8  
     1.9 @@ -153,15 +152,15 @@
    1.10  
    1.11  (*Tactic for possibility theorems*)
    1.12  ML {*
    1.13 -fun possibility_tac st = st |>
    1.14 +fun possibility ctxt =
    1.15      REPEAT (*omit used_Says so that Nonces start from different traces!*)
    1.16 -    (ALLGOALS (simp_tac (@{simpset} delsimps [used_Says]))
    1.17 +    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says]))
    1.18       THEN
    1.19       REPEAT_FIRST (eq_assume_tac ORELSE' 
    1.20                     resolve_tac [refl, conjI, @{thm Nonce_supply}]));
    1.21  *}
    1.22  
    1.23 -method_setup possibility = {* Scan.succeed (K (SIMPLE_METHOD possibility_tac)) *}
    1.24 +method_setup possibility = {* Scan.succeed (SIMPLE_METHOD o possibility_tac) *}
    1.25      "for proving possibility theorems"
    1.26  
    1.27  end