src/HOL/Auth/Smartcard/ShoupRubinBella.thy

          REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
 
 *}
 
 method_setup prepare = {*
-    Method.no_args (Method.METHOD (fn facts => prepare_tac)) *}
+    Method.no_args (Method.SIMPLE_METHOD prepare_tac) *}
   "to launch a few simple facts that'll help the simplifier"
 
 method_setup parts_prepare = {*
-    Method.no_args (Method.METHOD (fn facts => parts_prepare_tac)) *}
+    Method.no_args (Method.SIMPLE_METHOD parts_prepare_tac) *}
   "additional facts to reason about parts"
 
 method_setup analz_prepare = {*
-    Method.no_args (Method.METHOD (fn facts => analz_prepare_tac)) *}
+    Method.no_args (Method.SIMPLE_METHOD analz_prepare_tac) *}
   "additional facts to reason about analz"
 
 
 
 lemma Spy_parts_keys [simp]: "evs \<in> srb \<Longrightarrow>  

 val analz_image_Key_Un_Nonce= thm "analz_image_Key_Un_Nonce"
 *}
 
 method_setup sc_analz_freshK = {*
     Method.ctxt_args (fn ctxt =>
-     (Method.METHOD
-      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
+     (Method.SIMPLE_METHOD
+      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
                           REPEAT_FIRST (rtac analz_image_freshK_lemma),
                           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,