1.1 --- a/src/HOL/Auth/Message.thy	Wed Apr 25 10:31:39 2001 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Fri Apr 27 17:16:21 2001 +0200
     1.3 @@ -143,15 +143,23 @@
     1.4  by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
     1.5  
     1.6  method_setup spy_analz = {*
     1.7 -    Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
     1.8 +    Method.ctxt_args (fn ctxt =>
     1.9 +        Method.METHOD (fn facts => 
    1.10 +            gen_spy_analz_tac (Classical.get_local_claset ctxt,
    1.11 +                               Simplifier.get_local_simpset ctxt) 1)) *}
    1.12      "for proving the Fake case when analz is involved"
    1.13  
    1.14  method_setup atomic_spy_analz = {*
    1.15 -    Method.no_args (Method.METHOD (fn facts => atomic_spy_analz_tac 1)) *}
    1.16 +    Method.ctxt_args (fn ctxt =>
    1.17 +        Method.METHOD (fn facts => 
    1.18 +            atomic_spy_analz_tac (Classical.get_local_claset ctxt,
    1.19 +                                  Simplifier.get_local_simpset ctxt) 1)) *}
    1.20      "for debugging spy_analz"
    1.21  
    1.22  method_setup Fake_insert_simp = {*
    1.23 -    Method.no_args (Method.METHOD (fn facts => Fake_insert_simp_tac 1)) *}
    1.24 +    Method.ctxt_args (fn ctxt =>
    1.25 +        Method.METHOD (fn facts =>
    1.26 +            Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1)) *}
    1.27      "for debugging spy_analz"
    1.28  
    1.29  end