diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Auth/Message.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -941,15 +941,15 @@
 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
 
 method_setup spy_analz = {*
-    Method.ctxt_args (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *}
+    Scan.succeed (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *}
     "for proving the Fake case when analz is involved"
 
 method_setup atomic_spy_analz = {*
-    Method.ctxt_args (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
+    Scan.succeed (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
     "for debugging spy_analz"
 
 method_setup Fake_insert_simp = {*
-    Method.ctxt_args (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
+    Scan.succeed (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
     "for debugging spy_analz"
 
 end