# HG changeset patch
# User blanchet
# Date 1384967282 -3600
# Node ID 59737a43e044fa162368b858470db3421cd16775
# Parent  3cad06ff414b877698b165adaf086829a143bb6c
support Negated_Conjecture as a TPTP role as well (e.g. for SMT proofs)

diff -r 3cad06ff414b -r 59737a43e044 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 20 18:08:01 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 20 18:08:02 2013 +0100
@@ -74,7 +74,7 @@
 fun add_line (name as (_, ss), role, t, rule, []) lines =
     (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
        definitions. *)
-    if role = Conjecture orelse role = Hypothesis then
+    if role = Conjecture orelse role = Negated_Conjecture orelse role = Hypothesis then
       (name, role, t, rule, []) :: lines
     else if role = Axiom then
       (* Facts are not proof lines. *)
@@ -226,10 +226,12 @@
           |> rpair (0, [])
           |-> fold_rev add_desired_line
           |> snd
-        val conjs = atp_proof |> map_filter (try (fn (name, Conjecture, _, _, []) => name))
+        val conjs =
+          atp_proof |> map_filter (fn (name, role, _, _, _) =>
+            if role = Conjecture orelse role = Negated_Conjecture then SOME name else NONE)
         val assms =
           atp_proof
-          |> map_filter (try (fn ((num, _), Hypothesis, t, _, []) => (raw_label_of_num num, t)))
+          |> map_filter (try (fn ((num, _), Hypothesis, t, _, _) => (raw_label_of_num num, t)))
         val bot = atp_proof |> List.last |> #1
         val refute_graph =
           atp_proof