1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Feb 05 12:27:10 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Feb 05 12:27:10 2012 +0100
     1.3 @@ -746,8 +746,11 @@
     1.4                         SOME facts =>
     1.5                         let
     1.6                           val failure =
     1.7 -                           UnsoundProof (is_type_enc_quasi_sound type_enc,
     1.8 -                                         facts)
     1.9 +                           if null facts then
    1.10 +                             ProofIncomplete
    1.11 +                           else
    1.12 +                             UnsoundProof (is_type_enc_quasi_sound type_enc,
    1.13 +                                           facts)
    1.14                         in
    1.15                           if debug then
    1.16                             (warning (string_for_failure failure); NONE)