src/HOL/Tools/res_axioms.ML

   val pairname : thm -> (string * thm)
   val skolem_thm : thm -> thm list
   val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list
   val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list
 
-  val meson_method_setup : (theory -> theory) list  (*Reconstruction.thy*)
-  val setup : (theory -> theory) list               (*Main.thy*)
+  val meson_method_setup : theory -> theory
+  val setup : theory -> theory
   end;
 
 structure ResAxioms : RES_AXIOMS =
  
 struct

 fun meson_meth ths ctxt =
   Method.SIMPLE_METHOD' HEADGOAL
     (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) (local_claset_of ctxt));
 
 val meson_method_setup =
- [Method.add_methods
-  [("meson", Method.thms_ctxt_args meson_meth, 
-    "The MESON resolution proof procedure")]];
+  Method.add_methods
+    [("meson", Method.thms_ctxt_args meson_meth, 
+      "The MESON resolution proof procedure")];
 
 
 
 (*** The Skolemization attribute ***)
 

 
 val setup_attrs = Attrib.add_attributes
  [("skolem", (skolem_global, skolem_local),
     "skolemization of a theorem")];
 
-val setup = [clause_cache_setup, setup_attrs];
+val setup = clause_cache_setup #> setup_attrs;
 
 end;