--- 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"