author | blanchet |
Mon, 18 Jun 2012 17:50:06 +0200 | |
changeset 48104 | d2173ff80c57 |
parent 48103 | 1a6d5cc66931 |
child 48105 | a0e4618d6fed |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 18 17:50:06 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 18 17:50:06 2012 +0200 @@ -764,8 +764,7 @@ SOME facts => let val failure = - if null facts then ProofIncomplete - else UnsoundProof (is_type_enc_sound type_enc, facts) + UnsoundProof (is_type_enc_sound type_enc, facts) in if debug then (warning (string_for_failure failure); NONE)