# HG changeset patch
# User wenzelm
# Date 1152356076 -7200
# Node ID a7964311f1fbb7ce065f57d2ede03495167f2409
# Parent  e23a3afaaa8ac473c04e828c803031275a1f39c5
tactic/method simpset: maintain proper context;

diff -r e23a3afaaa8a -r a7964311f1fb src/HOL/Auth/OtwayReesBella.thy
--- a/src/HOL/Auth/OtwayReesBella.thy	Sat Jul 08 12:54:35 2006 +0200
+++ b/src/HOL/Auth/OtwayReesBella.thy	Sat Jul 08 12:54:36 2006 +0200
@@ -262,11 +262,11 @@
 *}
 
 method_setup analz_freshCryptK = {*
-    Method.no_args
+    Method.ctxt_args (fn ctxt =>
      (Method.METHOD
       (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
                           REPEAT_FIRST (rtac analz_image_freshCryptK_lemma),
-                          ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
+                          ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
   "for proving useful rewrite rule"
 
 
diff -r e23a3afaaa8a -r a7964311f1fb src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Sat Jul 08 12:54:35 2006 +0200
+++ b/src/HOL/Auth/Public.thy	Sat Jul 08 12:54:36 2006 +0200
@@ -409,11 +409,11 @@
 *}
 
 method_setup analz_freshK = {*
-    Method.no_args
+    Method.ctxt_args (fn ctxt =>
      (Method.METHOD
       (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
                           REPEAT_FIRST (rtac analz_image_freshK_lemma),
-                          ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
+                          ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
     "for proving the Session Key Compromise theorem"
 
 subsection{*Specialized Methods for Possibility Theorems*}
diff -r e23a3afaaa8a -r a7964311f1fb src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Sat Jul 08 12:54:35 2006 +0200
+++ b/src/HOL/Auth/Shared.thy	Sat Jul 08 12:54:36 2006 +0200
@@ -264,11 +264,11 @@
 (*Specialized methods*)
 
 method_setup analz_freshK = {*
-    Method.no_args
+    Method.ctxt_args (fn ctxt =>
      (Method.METHOD
       (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
                           REPEAT_FIRST (rtac analz_image_freshK_lemma),
-                          ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
+                          ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
     "for proving the Session Key Compromise theorem"
 
 method_setup possibility = {*
diff -r e23a3afaaa8a -r a7964311f1fb src/HOL/Auth/Smartcard/ShoupRubin.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sat Jul 08 12:54:35 2006 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sat Jul 08 12:54:36 2006 +0200
@@ -835,15 +835,15 @@
 *}
 
 method_setup sc_analz_freshK = {*
-    Method.no_args
+    Method.ctxt_args (fn ctxt =>
      (Method.METHOD
       (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
                           REPEAT_FIRST (rtac analz_image_freshK_lemma),
-                          ALLGOALS (asm_simp_tac (analz_image_freshK_ss
+                          ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss
                                     addsimps [knows_Spy_Inputs_secureM_sr_Spy,
                                               knows_Spy_Outpts_secureM_sr_Spy,
                                               shouprubin_assumes_securemeans, 
-                                              analz_image_Key_Un_Nonce]))])) *}
+                                              analz_image_Key_Un_Nonce]))]))) *}
     "for proving the Session Key Compromise theorem for smartcard protocols"
 
 
diff -r e23a3afaaa8a -r a7964311f1fb src/HOL/Auth/Smartcard/ShoupRubinBella.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Sat Jul 08 12:54:35 2006 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Sat Jul 08 12:54:36 2006 +0200
@@ -844,15 +844,15 @@
 *}
 
 method_setup sc_analz_freshK = {*
-    Method.no_args
+    Method.ctxt_args (fn ctxt =>
      (Method.METHOD
       (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
                           REPEAT_FIRST (rtac analz_image_freshK_lemma),
-                          ALLGOALS (asm_simp_tac (analz_image_freshK_ss
+                          ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss
                                     addsimps [knows_Spy_Inputs_secureM_srb_Spy,
                                               knows_Spy_Outpts_secureM_srb_Spy,
                                               shouprubin_assumes_securemeans, 
-                                              analz_image_Key_Un_Nonce]))])) *}
+                                              analz_image_Key_Un_Nonce]))]))) *}
     "for proving the Session Key Compromise theorem for smartcard protocols"
 
 
diff -r e23a3afaaa8a -r a7964311f1fb src/HOL/Auth/Smartcard/Smartcard.thy
--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Sat Jul 08 12:54:35 2006 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Sat Jul 08 12:54:36 2006 +0200
@@ -441,11 +441,11 @@
 (*Specialized methods*)
 
 method_setup analz_freshK = {*
-    Method.no_args
+    Method.ctxt_args (fn ctxt =>
      (Method.METHOD
       (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
                           REPEAT_FIRST (rtac analz_image_freshK_lemma),
-                          ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
+                          ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
     "for proving the Session Key Compromise theorem"
 
 method_setup possibility = {*
diff -r e23a3afaaa8a -r a7964311f1fb src/HOL/SET-Protocol/PublicSET.thy
--- a/src/HOL/SET-Protocol/PublicSET.thy	Sat Jul 08 12:54:35 2006 +0200
+++ b/src/HOL/SET-Protocol/PublicSET.thy	Sat Jul 08 12:54:36 2006 +0200
@@ -360,13 +360,13 @@
                    resolve_tac [refl, conjI, Nonce_supply]))
 
 (*Tactic for possibility theorems (ML script version)*)
-fun possibility_tac state = gen_possibility_tac (simpset()) state
+fun possibility_tac state = gen_possibility_tac (simpset_of (Thm.theory_of_thm state)) state
 
 (*For harder protocols (such as SET_CR!), where we have to set up some
   nonces and keys initially*)
 fun basic_possibility_tac st = st |>
     REPEAT 
-    (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
+    (ALLGOALS (asm_simp_tac (simpset_of (Thm.theory_of_thm st) setSolver safe_solver))
      THEN
      REPEAT_FIRST (resolve_tac [refl, conjI]))
 *}