src/HOL/Tools/Sledgehammer/sledgehammer.ML

     val (outcome, message) = Timeout.apply hard_timeout go ()
     val () = check_expected_outcome ctxt prover_name expect outcome
 
     val message = message ()
     val () =
-      (case outcome of
-        SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message)
-      | _ => ())
+      if mode = Auto_Try then
+        ()
+      else
+        (case outcome of
+          SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message)
+        | _ => ())
   in
     (outcome, message)
   end
 
 fun string_of_facts filter facts =

         (launch_provers ()
          handle Timeout.TIMEOUT _ => (SH_Timeout, ""))
         |> `(fn (outcome, _) =>
           (case outcome of
             SH_Some _ => (print "QED"; true)
-          | _ => (print "Sorry"; false)))
+          | _ => (print "No proof found"; false)))
       end)
 
 end;