# HG changeset patch
# User blanchet
# Date 1305793453 -7200
# Node ID 06d3ce527d290f4e4adc1c49390e0d10d512e836
# Parent  dfed4dbe559608e8168e74d1220cc52af865b818
tuning

diff -r dfed4dbe5596 -r 06d3ce527d29 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu May 19 10:24:13 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu May 19 10:24:13 2011 +0200
@@ -132,7 +132,7 @@
                   (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
                    else ""))
 
-fun neg_clausify ctxt =
+val neg_clausify =
   single
   #> Meson.make_clauses_unsorted
   #> map Meson_Clausify.introduce_combinators_in_theorem
@@ -158,7 +158,7 @@
       (verbose_warning ctxt "Proof state contains the universal sort {}";
        Seq.empty)
     else
-      Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt))
+      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
                   ctxt i st0
   end