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