--- 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"
--- 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*}
--- 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 = {*
--- 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"
--- 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"
--- 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 = {*
--- 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]))
*}