1.1 --- a/doc-src/TutorialI/Protocol/Public.thy	Thu Jul 23 18:44:08 2009 +0200
     1.2 +++ b/doc-src/TutorialI/Protocol/Public.thy	Thu Jul 23 18:44:09 2009 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4  ML {*
     1.5  fun possibility_tac ctxt =
     1.6      REPEAT (*omit used_Says so that Nonces start from different traces!*)
     1.7 -    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says]))
     1.8 +    (ALLGOALS (simp_tac (simpset_of ctxt delsimps [used_Says]))
     1.9       THEN
    1.10       REPEAT_FIRST (eq_assume_tac ORELSE' 
    1.11                     resolve_tac [refl, conjI, @{thm Nonce_supply}]));