# HG changeset patch
# User blanchet
# Date 1351679001 -3600
# Node ID ceceb403eb4ecf29eafb8b10ebd25903fbc74ebb
# Parent  80402e0e78e388afdf09236f6f827cb5b240230b
fixed bool vs. prop mismatch

diff -r 80402e0e78e3 -r ceceb403eb4e src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -889,14 +889,14 @@
                           if member (op = o apsnd fst) tainted s then
                             t |> s_not
                               |> fold exists_of (map Var (Term.add_vars t []))
-                              |> HOLogic.mk_Trueprop
                           else
-                            t |> HOLogic.mk_Trueprop
-                              |> close_form))
+                            t))
                   atp_proof
         fun prop_of_clause c =
           fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)
                @{term False}
+          |> HOLogic.mk_Trueprop
+          |> close_form
         fun label_of_clause [name] = raw_label_for_name name
           | label_of_clause c = (space_implode "___" (map fst c), 0)
         fun maybe_show outer c =