# HG changeset patch
# User paulson
# Date 1086772763 -7200
# Node ID 51f28df21c8bb4467a5809d8610f52391466e77a
# Parent  d7711d6b901448f9bf256e1d648f4ca5a7fe414d
fixed the skolemize method

diff -r d7711d6b9014 -r 51f28df21c8b src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Jun 09 11:18:51 2004 +0200
+++ b/src/HOL/Tools/meson.ML	Wed Jun 09 11:19:23 2004 +0200
@@ -408,13 +408,17 @@
   Method.SIMPLE_METHOD' HEADGOAL
     (CHANGED_PROP o meson_claset_tac (Classical.get_local_claset ctxt));
 
+val skolemize_meth =
+  Method.SIMPLE_METHOD' HEADGOAL
+    (CHANGED_PROP o skolemize_tac);
+
 in
 
 val meson_setup =
  [Method.add_methods
   [("meson", Method.ctxt_args meson_meth, 
     "The MESON resolution proof procedure"),
-   ("skolemize", Method.no_args (Method.METHOD (fn _ => skolemize_tac 1)), 
+   ("skolemize", Method.no_args skolemize_meth, 
     "Skolemization into existential quantifiers")]];
 
 end;