changeset 46427 | 4fd25dadbd94 |
parent 46409 | d4754183ccce |
child 46442 | 1e07620d724c |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Feb 05 12:27:10 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Feb 05 12:27:10 2012 +0100 @@ -746,8 +746,11 @@ SOME facts => let val failure = - UnsoundProof (is_type_enc_quasi_sound type_enc, - facts) + if null facts then + ProofIncomplete + else + UnsoundProof (is_type_enc_quasi_sound type_enc, + facts) in if debug then (warning (string_for_failure failure); NONE)