# HG changeset patch
# User blanchet
# Date 1677654051 -3600
# Node ID 4a6eb1b1834060f84e8e721beeba56e996f0f1e4
# Parent  bde374587d939edeb6a894c0529c9d9823cc7118
avoid double 'Warning:' in Sledgehammer messages

diff -r bde374587d93 -r 4a6eb1b18340 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -334,10 +334,10 @@
       else
         (really_go ()
          handle
-           ERROR msg => (SH_Unknown, fn () => "Warning: " ^ msg ^ "\n")
+           ERROR msg => (SH_Unknown, fn () => msg ^ "\n")
          | exn =>
            if Exn.is_interrupt exn then Exn.reraise exn
-           else (SH_Unknown, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
+           else (SH_Unknown, fn () => Runtime.exn_message exn ^ "\n"))
 
     val (outcome, message) = Timeout.apply hard_timeout go ()
     val () = check_expected_outcome ctxt prover_name expect outcome