src/HOL/SET-Protocol/MessageSET.thy
changeset 15032 02aed07e01bf
parent 14218 db95d1c2f51b
child 16417 9bc16273c2d4
--- a/src/HOL/SET-Protocol/MessageSET.thy	Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Sun Jul 11 20:33:22 2004 +0200
@@ -936,21 +936,19 @@
 method_setup spy_analz = {*
     Method.ctxt_args (fn ctxt =>
         Method.METHOD (fn facts =>
-            gen_spy_analz_tac (Classical.get_local_claset ctxt,
-                               Simplifier.get_local_simpset ctxt) 1))*}
+            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 (Classical.get_local_claset ctxt,
-                                  Simplifier.get_local_simpset ctxt) 1))*}
+            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 (Simplifier.get_local_simpset ctxt) 1))*}
+            Fake_insert_simp_tac (local_simpset_of ctxt) 1))*}
     "for debugging spy_analz"