src/HOL/Tools/ATP/atp_systems.ML

--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu May 10 10:07:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu May 10 10:07:40 2012 +0200
@@ -337,7 +337,7 @@
      [(TimedOut, "CPU time limit exceeded, terminating"),
       (GaveUp, "No.of.Axioms")],
    conj_sym_kind = Axiom,
-   prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *),
+   prem_kind = Hypothesis,
    best_slices = fn ctxt =>
      (* FUDGE *)
      [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", keep_lamsN, false), sosN))),