diff -r 4c2514625873 -r 2eef5e71edd6 doc-src/TutorialI/Protocol/Message.thy --- a/doc-src/TutorialI/Protocol/Message.thy Mon Mar 16 17:51:07 2009 +0100 +++ b/doc-src/TutorialI/Protocol/Message.thy Mon Mar 16 17:51:24 2009 +0100 @@ -919,15 +919,15 @@ lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] method_setup spy_analz = {* - Method.ctxt_args (SIMPLE_METHOD' o gen_spy_analz_tac o local_clasimpset_of) *} + Scan.succeed (SIMPLE_METHOD' o 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 atomic_spy_analz_tac o local_clasimpset_of) *} + Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac o local_clasimpset_of) *} "for debugging spy_analz" method_setup Fake_insert_simp = {* - Method.ctxt_args (SIMPLE_METHOD' o Fake_insert_simp_tac o local_simpset_of) *} + Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o local_simpset_of) *} "for debugging spy_analz"