1.1 --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Feb 20 16:21:04 2013 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Feb 20 17:05:24 2013 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  
     1.5    type direct_proof = direct_inference list
     1.6  
     1.7 -  val make_refute_graph : (atom list * atom) list -> refute_graph
     1.8 +  val make_refute_graph : atom -> (atom list * atom) list -> refute_graph
     1.9    val axioms_of_refute_graph : refute_graph -> atom list -> atom list
    1.10    val tainted_atoms_of_refute_graph : refute_graph -> atom list -> atom list
    1.11    val sequents_of_refute_graph : refute_graph -> ref_sequent list
    1.12 @@ -72,14 +72,16 @@
    1.13  fun direct_sequent_eq ((gamma, c), (delta, d)) =
    1.14    clause_eq (gamma, delta) andalso clause_eq (c, d)
    1.15  
    1.16 -fun make_refute_graph infers =
    1.17 +fun make_refute_graph bot infers =
    1.18    let
    1.19      fun add_edge to from =
    1.20        Atom_Graph.default_node (from, ())
    1.21        #> Atom_Graph.default_node (to, ())
    1.22        #> Atom_Graph.add_edge_acyclic (from, to)
    1.23      fun add_infer (froms, to) = fold (add_edge to) froms
    1.24 -  in Atom_Graph.empty |> fold add_infer infers end
    1.25 +    val graph = fold add_infer infers Atom_Graph.empty
    1.26 +    val reachable = Atom_Graph.all_preds graph [bot]
    1.27 +  in graph |> Atom_Graph.restrict (member (is_equal o Atom.ord) reachable) end
    1.28  
    1.29  fun axioms_of_refute_graph refute_graph conjs =
    1.30    subtract atom_eq conjs (Atom_Graph.minimals refute_graph)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 16:21:04 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 17:05:24 2013 +0100
     2.3 @@ -678,12 +678,12 @@
     2.4                   | _ => NONE)
     2.5                | _ => NONE)
     2.6          fun dep_of_step (name, _, _, _, from) = SOME (from, name)
     2.7 +        val bot = atp_proof |> List.last |> dep_of_step |> the |> snd
     2.8          val refute_graph =
     2.9 -          atp_proof |> map_filter dep_of_step |> make_refute_graph
    2.10 +          atp_proof |> map_filter dep_of_step |> make_refute_graph bot
    2.11          val axioms = axioms_of_refute_graph refute_graph conjs
    2.12          val tainted = tainted_atoms_of_refute_graph refute_graph conjs
    2.13          val is_clause_tainted = exists (member (op =) tainted)
    2.14 -        val bot = atp_proof |> List.last |> dep_of_step |> the |> snd
    2.15          val steps =
    2.16            Symtab.empty
    2.17            |> fold (fn (name as (s, _), role, t, rule, _) =>