# HG changeset patch
# User blanchet
# Date 1643723671 -3600
# Node ID ec18dcd6e85f9a1c4ef3fc8924a1f7a84592e0df
# Parent  95e3aade547d95abd6a8c59573dd0693e878ff1e
don't lose error messages

diff -r 95e3aade547d -r ec18dcd6e85f src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Feb 01 12:49:14 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Feb 01 14:54:31 2022 +0100
@@ -452,9 +452,10 @@
       in
         (launch_provers ()
          handle Timeout.TIMEOUT _ => (SH_Timeout, ""))
-        |> `(fn (outcome, _) =>
+        |> `(fn (outcome, message) =>
           (case outcome of
             SH_Some _ => (print "QED"; true)
+          | SH_Unknown => (print message; false)
           | _ => (print "No proof found"; false)))
       end)