don't lose error messages
authorblanchet
Tue, 01 Feb 2022 14:54:31 +0100
changeset 75054 ec18dcd6e85f
parent 75053 95e3aade547d
child 75055 c84a20e9b00f
don't lose error messages
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)