doc-src/TutorialI/Protocol/Public.thy

--- a/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 13 19:10:46 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Public.thy	Fri Mar 13 19:53:09 2009 +0100
@@ -161,8 +161,7 @@
                    resolve_tac [refl, conjI, @{thm Nonce_supply}]));
 *}
 
-method_setup possibility = {*
-    Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
+method_setup possibility = {* Method.no_args (SIMPLE_METHOD possibility_tac) *}
     "for proving possibility theorems"
 
 end