src/HOL/Auth/OtwayReesBella.thy

 	       delsimps [imp_disjL]    (*reduces blow-up*)
 	       addsimps thms "analz_image_freshK_simps"
 *}
 
 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"
 
 
 method_setup disentangle = {*
     Method.no_args