# HG changeset patch
# User blanchet
# Date 1335525535 -7200
# Node ID 35fcb0daab8d07289f6a86f8b7508020a6b7a7ea
# Parent  034cc7cc8b4a854e31d270dfa38b9a268a621b18
tweak LEO-II setup

diff -r 034cc7cc8b4a -r 35fcb0daab8d src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Apr 27 12:16:10 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Apr 27 13:18:55 2012 +0200
@@ -390,6 +390,8 @@
               | File_Source _ =>
                 ((num, find_formula_in_problem problem phi), "", [])
               | Inference_Source (rule, deps) => ((num, []), rule, deps)
+            fun mk_step () =
+              Inference_Step (name, phi, rule, map (rpair []) deps)
           in
             case role of
               "definition" =>
@@ -399,8 +401,8 @@
                | AAtom (ATerm ("equal", _)) =>
                  (* Vampire's equality proxy axiom *)
                  Inference_Step (name, phi, rule, map (rpair []) deps)
-               | _ => raise UNRECOGNIZED_ATP_PROOF ())
-            | _ => Inference_Step (name, phi, rule, map (rpair []) deps)
+               | _ => mk_step ())
+            | _ => mk_step ()
           end)
 
 (**** PARSING OF SPASS OUTPUT ****)
diff -r 034cc7cc8b4a -r 35fcb0daab8d src/HOL/Tools/ATP/atp_systems.ML
--- 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)}