# HG changeset patch
# User blanchet
# Date 1337800788 -7200
# Node ID 08d2dcc2dab907e3c5d94e0b953f0b857fe9badb
# Parent  9af7e5caf16f767f0864a2e304776a381eb44f7b
improved LEO-II definition handling -- still hoping for a fix directly in LEO-II

diff -r 9af7e5caf16f -r 08d2dcc2dab9 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed May 23 21:19:48 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed May 23 21:19:48 2012 +0200
@@ -481,15 +481,6 @@
            | Fail "inappropriate" => failed ATP_Proof.Inappropriate
     val time_prover = run_time |> Time.toMilliseconds
     val msg = message (preplay ()) ^ message_tail
-    val (outcome, used_facts) =
-      (* Repair incomplete or missing proofs. Better do it here and not in
-         Sledgehammer, so that actual Sledgehammer users get a chance to report
-         the issue. FIXME: This is a temporary hack. *)
-      if outcome = SOME ATP_Proof.ProofIncomplete orelse
-         outcome = SOME ATP_Proof.ProofMissing then
-        (NONE, [])
-      else
-        (outcome, used_facts)
   in
     case outcome of
       NONE => (msg, SH_OK (time_isa, time_prover, used_facts))
diff -r 9af7e5caf16f -r 08d2dcc2dab9 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed May 23 21:19:48 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed May 23 21:19:48 2012 +0200
@@ -188,6 +188,8 @@
   is_axiom_used_in_proof is_typed_helper_name atp_proof
 
 val leo2_ext = "extcnf_equal_neg"
+val leo2_unfold_def = "unfold_def"
+
 val isa_ext = Thm.get_name_hint @{thm ext}
 val isa_short_ext = Long_Name.base_name isa_ext
 
@@ -198,17 +200,24 @@
   else
     isa_ext
 
+fun add_all_defs fact_names accum =
+  Vector.foldl (fn (facts, factss) =>
+                   filter (fn (_, (_, status)) => status = Def) facts @ factss)
+               accum fact_names
+
 fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, rule, deps)) =
     (if rule = leo2_ext then
        insert (op =) (ext_name ctxt, (Global, General))
+     else if rule = leo2_unfold_def then
+       (* LEO 1.3.3 does not record definitions properly, leading to missing
+         dependencies in the TSTP proof. Remove the next line once this is
+         fixed. *)
+       add_all_defs fact_names
      else if rule = satallax_unsat_coreN then
        (fn [] =>
            (* Satallax doesn't include definitions in its unsatisfiable cores,
               so we assume the worst and include them all here. *)
-           Vector.foldl (fn (facts, factss) =>
-                            filter (fn (_, (_, status)) => status = Def) facts
-                            @ factss)
-                        [(ext_name ctxt, (Global, General))] fact_names
+           [(ext_name ctxt, (Global, General))] |> add_all_defs fact_names
          | facts => facts)
      else
        I)
diff -r 9af7e5caf16f -r 08d2dcc2dab9 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed May 23 21:19:48 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed May 23 21:19:48 2012 +0200
@@ -337,11 +337,7 @@
         "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
-     [(* LEO 1.3.3 does not record definitions properly, leading to missing
-         dependencies in the TSTP proof. Remove the next line once this is
-         fixed. *)
-      (ProofIncomplete, "_def,definition,"),
-      (TimedOut, "CPU time limit exceeded, terminating"),
+     [(TimedOut, "CPU time limit exceeded, terminating"),
       (GaveUp, "No.of.Axioms")] @
      known_szs_status_failures,
    prem_kind = Hypothesis,