src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

                    [j] =>
                    if j = length hyp_ts then NONE
                    else SOME (raw_label_for_name name, nth hyp_ts j)
                  | _ => NONE)
               | _ => NONE)
-        fun dep_of_step (name, _, _, _, from) = SOME (from, name)
-        val bot = atp_proof |> List.last |> dep_of_step |> the |> snd
+        val bot = atp_proof |> List.last |> #1
         val refute_graph =
-          atp_proof |> map_filter dep_of_step |> make_refute_graph bot
+          atp_proof
+          |> map (fn (name, _, _, _, from) => (from, name))
+          |> make_refute_graph bot
+          |> fold (Atom_Graph.default_node o rpair ()) conjs
         val axioms = axioms_of_refute_graph refute_graph conjs
         val tainted = tainted_atoms_of_refute_graph refute_graph conjs
         val is_clause_tainted = exists (member (op =) tainted)
         val steps =
           Symtab.empty

             let
               val lits = map snd (map_filter (Symtab.lookup steps o fst) names)
             in
               case List.partition (can HOLogic.dest_not) lits of
                 (negs as _ :: _, pos as _ :: _) =>
-                HOLogic.mk_imp
-                  (Library.foldr1 s_conj (map HOLogic.dest_not negs),
-                   Library.foldr1 s_disj pos)
+                s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs),
+                       Library.foldr1 s_disj pos)
               | _ => fold (curry s_disj) lits @{term False}
             end
             |> HOLogic.mk_Trueprop |> close_form
         fun isar_proof_of_direct_proof infs =
           let