1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 20 18:08:01 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 20 18:08:02 2013 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4  fun add_line (name as (_, ss), role, t, rule, []) lines =
     1.5      (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
     1.6         definitions. *)
     1.7 -    if role = Conjecture orelse role = Hypothesis then
     1.8 +    if role = Conjecture orelse role = Negated_Conjecture orelse role = Hypothesis then
     1.9        (name, role, t, rule, []) :: lines
    1.10      else if role = Axiom then
    1.11        (* Facts are not proof lines. *)
    1.12 @@ -226,10 +226,12 @@
    1.13            |> rpair (0, [])
    1.14            |-> fold_rev add_desired_line
    1.15            |> snd
    1.16 -        val conjs = atp_proof |> map_filter (try (fn (name, Conjecture, _, _, []) => name))
    1.17 +        val conjs =
    1.18 +          atp_proof |> map_filter (fn (name, role, _, _, _) =>
    1.19 +            if role = Conjecture orelse role = Negated_Conjecture then SOME name else NONE)
    1.20          val assms =
    1.21            atp_proof
    1.22 -          |> map_filter (try (fn ((num, _), Hypothesis, t, _, []) => (raw_label_of_num num, t)))
    1.23 +          |> map_filter (try (fn ((num, _), Hypothesis, t, _, _) => (raw_label_of_num num, t)))
    1.24          val bot = atp_proof |> List.last |> #1
    1.25          val refute_graph =
    1.26            atp_proof