changeset 44915 | 635ae0a73688 |
parent 44858 | d615dfa88572 |
child 45299 | ee584ff987c3 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Sep 13 09:56:38 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Sep 13 11:24:58 2011 +0200 @@ -696,9 +696,8 @@ SOME facts => let val failure = - (if is_type_enc_quasi_sound type_enc then SOME sound - else NONE, facts) - |> UnsoundProof + UnsoundProof (is_type_enc_quasi_sound type_enc, + facts) in if debug then (warning (string_for_failure failure); NONE)