diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Auth/Public.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -424,7 +424,7 @@
 *}
 
 method_setup analz_freshK = {*
-    Method.ctxt_args (fn ctxt =>
+    Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
           REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
@@ -435,11 +435,11 @@
 subsection{*Specialized Methods for Possibility Theorems*}
 
 method_setup possibility = {*
-    Method.ctxt_args (SIMPLE_METHOD o Public.possibility_tac) *}
+    Scan.succeed (SIMPLE_METHOD o Public.possibility_tac) *}
     "for proving possibility theorems"
 
 method_setup basic_possibility = {*
-    Method.ctxt_args (SIMPLE_METHOD o Public.basic_possibility_tac) *}
+    Scan.succeed (SIMPLE_METHOD o Public.basic_possibility_tac) *}
     "for proving possibility theorems"
 
 end