src/HOL/Tools/ATP/atp_systems.ML
changeset 47787 35fcb0daab8d
parent 47772 993a44ef9928
child 47898 6213900d6d5f
--- 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)}