src/HOL/Auth/Message.thy
changeset 21588 cd0dc678a205
parent 20648 742c30fc3fcb
child 22424 8a5412121687
     1.1 --- a/src/HOL/Auth/Message.thy	Wed Nov 29 15:44:46 2006 +0100
     1.2 +++ b/src/HOL/Auth/Message.thy	Wed Nov 29 15:44:51 2006 +0100
     1.3 @@ -948,20 +948,17 @@
     1.4  
     1.5  method_setup spy_analz = {*
     1.6      Method.ctxt_args (fn ctxt =>
     1.7 -        Method.METHOD (fn facts => 
     1.8 -            gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
     1.9 +        Method.SIMPLE_METHOD (gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    1.10      "for proving the Fake case when analz is involved"
    1.11  
    1.12  method_setup atomic_spy_analz = {*
    1.13      Method.ctxt_args (fn ctxt =>
    1.14 -        Method.METHOD (fn facts => 
    1.15 -            atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    1.16 +        Method.SIMPLE_METHOD (atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    1.17      "for debugging spy_analz"
    1.18  
    1.19  method_setup Fake_insert_simp = {*
    1.20      Method.ctxt_args (fn ctxt =>
    1.21 -        Method.METHOD (fn facts =>
    1.22 -            Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
    1.23 +        Method.SIMPLE_METHOD (Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
    1.24      "for debugging spy_analz"
    1.25  
    1.26