--- 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 ****)
--- 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)}