src/HOL/Auth/Message.thy
changeset 15032 02aed07e01bf
parent 14200 d8598e24f8fa
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Auth/Message.thy	Fri Jul 09 16:33:20 2004 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Sun Jul 11 20:33:22 2004 +0200
     1.3 @@ -932,21 +932,19 @@
     1.4  method_setup spy_analz = {*
     1.5      Method.ctxt_args (fn ctxt =>
     1.6          Method.METHOD (fn facts => 
     1.7 -            gen_spy_analz_tac (Classical.get_local_claset ctxt,
     1.8 -                               Simplifier.get_local_simpset ctxt) 1)) *}
     1.9 +            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 (Classical.get_local_claset ctxt,
    1.16 -                                  Simplifier.get_local_simpset ctxt) 1)) *}
    1.17 +            atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    1.18      "for debugging spy_analz"
    1.19  
    1.20  method_setup Fake_insert_simp = {*
    1.21      Method.ctxt_args (fn ctxt =>
    1.22          Method.METHOD (fn facts =>
    1.23 -            Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1)) *}
    1.24 +            Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
    1.25      "for debugging spy_analz"
    1.26  
    1.27