diff -r a3561bfe0ada -r cd0dc678a205 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Nov 29 15:44:46 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Wed Nov 29 15:44:51 2006 +0100
@@ -608,14 +608,10 @@
 
 fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths);
 
-fun meson_meth ths ctxt =
-  Method.SIMPLE_METHOD' HEADGOAL
-    (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs);
-
-val meson_method_setup =
-  Method.add_methods
-    [("meson", Method.thms_ctxt_args meson_meth,
-      "MESON resolution proof procedure")];
+val meson_method_setup = Method.add_methods
+  [("meson", Method.thms_args (fn ths =>
+      Method.SIMPLE_METHOD' (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs)),
+    "MESON resolution proof procedure")];
 
 (** Attribute for converting a theorem into clauses **)