doc-src/TutorialI/Protocol/Public.thy

--- a/doc-src/TutorialI/Protocol/Public.thy	Mon Mar 16 17:51:07 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Public.thy	Mon Mar 16 17:51:24 2009 +0100
@@ -161,7 +161,7 @@
                    resolve_tac [refl, conjI, @{thm Nonce_supply}]));
 *}
 
-method_setup possibility = {* Method.no_args (SIMPLE_METHOD possibility_tac) *}
+method_setup possibility = {* Scan.succeed (K (SIMPLE_METHOD possibility_tac)) *}
     "for proving possibility theorems"
 
 end