--- a/src/HOL/Auth/Message.thy Wed Nov 29 15:44:46 2006 +0100
+++ b/src/HOL/Auth/Message.thy Wed Nov 29 15:44:51 2006 +0100
@@ -948,20 +948,17 @@
method_setup spy_analz = {*
Method.ctxt_args (fn ctxt =>
- Method.METHOD (fn facts =>
- gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
+ Method.SIMPLE_METHOD (gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
Method.ctxt_args (fn ctxt =>
- Method.METHOD (fn facts =>
- atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
+ Method.SIMPLE_METHOD (atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
Method.ctxt_args (fn ctxt =>
- Method.METHOD (fn facts =>
- Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
+ Method.SIMPLE_METHOD (Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
"for debugging spy_analz"