# HG changeset patch
# User blanchet
# Date 1272309500 -7200
# Node ID 31252c4d49239a9010a6d0ae51525704582c2f4d
# Parent  c5bae529f9673cf4be174b8dc1e2b860d76d4c66
adapt code to reflect new signature of "neg_clausify"

diff -r c5bae529f967 -r 31252c4d4923 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Apr 26 21:17:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Apr 26 21:18:20 2010 +0200
@@ -721,7 +721,7 @@
     if exists_type type_has_topsort (prop_of st0)
     then raise METIS "Metis: Proof state contains the universal sort {}"
     else
-      (Meson.MESON neg_clausify
+      (Meson.MESON (maps neg_clausify)
         (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
           THEN Meson_Tactic.expand_defs_tac st0) st0
   end