src/HOL/Auth/OtwayReesBella.thy

     forward_tac [@{thm OR4_parts_knows_Spy}]  (i+6) THEN
     forward_tac [@{thm OR2_parts_knows_Spy}]  (i+4)
 *}
  
 method_setup parts_explicit = {*
-    Method.no_args (Method.SIMPLE_METHOD' parts_explicit_tac) *}
+    Method.no_args (SIMPLE_METHOD' parts_explicit_tac) *}
   "to explicitly state that some message components belong to parts knows Spy"
 
 
 lemma Spy_see_shrK [simp]: 
     "evs \<in> orb \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"

 end
 *}
 
 method_setup analz_freshCryptK = {*
     Method.ctxt_args (fn ctxt =>
-     (Method.SIMPLE_METHOD
+     (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
           REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
           ALLGOALS (asm_simp_tac
             (Simplifier.context ctxt OtwayReesBella.analz_image_freshK_ss))]))) *}
   "for proving useful rewrite rule"
 
 
 method_setup disentangle = {*
     Method.no_args
-     (Method.SIMPLE_METHOD
+     (SIMPLE_METHOD
       (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
                    ORELSE' hyp_subst_tac))) *}
   "for eliminating conjunctions, disjunctions and the like"