--- 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