# HG changeset patch
# User blanchet
# Date 1361378540 -3600
# Node ID 2bbcc9cc12b46f2e0a65170e65ba2076959e545b
# Parent  e5ef7a18f4a3c88bbbec158d5203dc703e3e831a
ensure all conjecture clauses are in the graph -- to prevent exceptions later

diff -r e5ef7a18f4a3 -r 2bbcc9cc12b4 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 17:31:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 17:42:20 2013 +0100
@@ -677,10 +677,12 @@
                    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)
@@ -711,9 +713,8 @@
             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