diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Thu Jan 19 21:22:08 2006 +0100
@@ -27,8 +27,8 @@
   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 =
@@ -471,9 +471,9 @@
     (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")];
 
 
 
@@ -497,6 +497,6 @@
  [("skolem", (skolem_global, skolem_local),
     "skolemization of a theorem")];
 
-val setup = [clause_cache_setup, setup_attrs];
+val setup = clause_cache_setup #> setup_attrs;
 
 end;