changeset 48104 | d2173ff80c57 |
parent 48089 | fcb2292aa260 |
child 48130 | defbcdc60fd6 |
--- 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)