--- 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