# HG changeset patch
# User blanchet
# Date 1340034606 -7200
# Node ID d2173ff80c5748c288177f4e5c922d2b2518622b
# Parent  1a6d5cc6693137c82ccda60a9ebebc4503b9eccb
less confusing error message

diff -r 1a6d5cc66931 -r d2173ff80c57 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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)