src/HOL/Tools/res_axioms.ML

     val thy = Thm.theory_of_thm st0
   in  (Meson.meson_claset_tac (maps (cnf_axiom thy) ths) HOL_cs i THEN expand_defs_tac st0) st0 end;
 
 val meson_method_setup = Method.add_methods
   [("meson", Method.thms_args (fn ths =>
-      Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
+      SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
     "MESON resolution proof procedure")];
 
 
 (*** Converting a subgoal into negated conjecture clauses. ***)
 

                 (map forall_intr_vars (neg_clausify hyps)) 1)),
           REPEAT_DETERM_N (length ts) o (etac thin_rl)]
      end);
 
 val setup_methods = Method.add_methods
-  [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
+  [("neg_clausify", Method.no_args (SIMPLE_METHOD' neg_clausify_tac),
     "conversion of goal to conjecture clauses")];
 
 
 (** Attribute for converting a theorem into clauses **)