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