# HG changeset patch
# User blanchet
# Date 1337592712 -7200
# Node ID 7b482cc7473e6237c9b7c5e0c325d77113d2a900
# Parent  33afcfad3f8de837101ec846effd3ad297e7e92e
include "ext" in all Satallax proofs

diff -r 33afcfad3f8d -r 7b482cc7473e src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 21 10:39:32 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 21 11:31:52 2012 +0200
@@ -51,6 +51,7 @@
     -> string * failure option
   val is_same_atp_step : step_name -> step_name -> bool
   val scan_general_id : string list -> string * string list
+  val satallax_unsat_coreN : string
   val parse_formula :
     string list -> (string, 'a, (string, 'a) ho_term) formula * string list
   val atp_proof_from_tstplike_proof :
@@ -465,10 +466,13 @@
          Inference_Step ((num, resolve_spass_num names spass_names num), u,
              rule, map (swap o `(resolve_spass_num NONE spass_names)) deps))
 
+val satallax_unsat_coreN = "__satallax_unsat_core" (* arbitrary *)
+
 (* Syntax: <name> *)
 fun parse_satallax_line x =
   (scan_general_id --| Scan.option ($$ " ")
-   >> (fn s => Inference_Step ((s, [s]), dummy_phi, "", []))) x
+   >> (fn s => Inference_Step ((s, [s]), dummy_phi, satallax_unsat_coreN, [])))
+      x
 
 fun parse_line problem spass_names =
   parse_tstp_line problem || parse_spass_line spass_names || parse_satallax_line
diff -r 33afcfad3f8d -r 7b482cc7473e src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 21 10:39:32 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 21 11:31:52 2012 +0200
@@ -198,11 +198,13 @@
   else
     isa_ext
 
-fun add_fact _ fact_names (Inference_Step ((_, ss), _, _, [])) =
-    union (op =) (resolve_fact fact_names ss)
-  | add_fact ctxt _ (Inference_Step (_, _, rule, _)) =
-    if rule = leo2_ext then insert (op =) (ext_name ctxt, (Global, General))
-    else I
+fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, rule, deps)) =
+    (if rule = leo2_ext orelse rule = satallax_unsat_coreN then
+       insert (op =) (ext_name ctxt, (Global, General))
+     else
+       I)
+    #> (if null deps then union (op =) (resolve_fact fact_names ss)
+        else I)
   | add_fact _ _ _ = I
 
 fun used_facts_in_atp_proof ctxt fact_names atp_proof =