--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Apr 27 12:16:10 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Apr 27 13:18:55 2012 +0200
@@ -337,11 +337,11 @@
[(TimedOut, "CPU time limit exceeded, terminating"),
(GaveUp, "No.of.Axioms")],
conj_sym_kind = Axiom,
- prem_kind = Hypothesis,
+ prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *),
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", liftingN, false), sosN))),
- (0.333, (true, ((50, leo2_thf0, "mono_native_higher", liftingN, false), no_sosN)))]
+ [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", keep_lamsN, false), sosN))),
+ (0.333, (true, ((50, leo2_thf0, "mono_native_higher", keep_lamsN, false), no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}