adapt code to reflect new signature of "neg_clausify"
authorblanchet
Mon, 26 Apr 2010 21:18:20 +0200
changeset 36401 31252c4d4923
parent 36400 c5bae529f967
child 36402 1b20805974c7
adapt code to reflect new signature of "neg_clausify"
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