--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 09 20:09:43 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 09 20:11:52 2010 +0200
@@ -816,6 +816,13 @@
#> map Clausifier.introduce_combinators_in_theorem
#> Meson.finish_cnf
+fun preskolem_tac ctxt st0 =
+ (if exists (Meson.has_too_many_clauses ctxt)
+ (Logic.prems_of_goal (prop_of st0) 1) then
+ cnf.cnfx_rewrite_tac ctxt 1
+ else
+ all_tac) st0
+
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
@@ -828,7 +835,7 @@
if exists_type type_has_top_sort (prop_of st0) then
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
else
- Meson.MESON (K all_tac) (maps neg_clausify)
+ Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
ctxt i st0
end