# HG changeset patch
# User blanchet
# Date 1352209581 -3600
# Node ID 4ea26c74d7eaabf927bbcf48a39b268b716d5280
# Parent  d9c1b11a78d2bfc43243dbeb141d3efd45af8982
use implications rather than disjunctions to improve readability

diff -r d9c1b11a78d2 -r 4ea26c74d7ea src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 13:47:51 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 14:46:21 2012 +0100
@@ -998,8 +998,14 @@
              | _ => the_default @{term False} (Symtab.lookup props s)
                     |> HOLogic.mk_Trueprop |> close_form)
           | prop_of_clause names =
-            fold (curry s_disj) (map_filter (Symtab.lookup props o fst) names)
-                 @{term False}
+            let val lits = map_filter (Symtab.lookup props 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)
+              | _ => fold (curry s_disj) lits @{term False}
+            end
             |> HOLogic.mk_Trueprop |> close_form
         fun maybe_show outer c =
           (outer andalso length c = 1 andalso subset (op =) (c, conjs))