1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 13:47:51 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 14:46:21 2012 +0100
     1.3 @@ -998,8 +998,14 @@
     1.4               | _ => the_default @{term False} (Symtab.lookup props s)
     1.5                      |> HOLogic.mk_Trueprop |> close_form)
     1.6            | prop_of_clause names =
     1.7 -            fold (curry s_disj) (map_filter (Symtab.lookup props o fst) names)
     1.8 -                 @{term False}
     1.9 +            let val lits = map_filter (Symtab.lookup props o fst) names in
    1.10 +              case List.partition (can HOLogic.dest_not) lits of
    1.11 +                (negs as _ :: _, pos as _ :: _) =>
    1.12 +                HOLogic.mk_imp
    1.13 +                  (Library.foldr1 s_conj (map HOLogic.dest_not negs),
    1.14 +                   Library.foldr1 s_disj pos)
    1.15 +              | _ => fold (curry s_disj) lits @{term False}
    1.16 +            end
    1.17              |> HOLogic.mk_Trueprop |> close_form
    1.18          fun maybe_show outer c =
    1.19            (outer andalso length c = 1 andalso subset (op =) (c, conjs))