# HG changeset patch
# User blanchet
# Date 1288879184 -3600
# Node ID 14456fd302f071a56d6e0f3f792d5f957d71672e
# Parent  53dca3bd425020136a5c0147ef203626a9109897
cosmetics

diff -r 53dca3bd4250 -r 14456fd302f0 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Nov 04 14:59:44 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Nov 04 14:59:44 2010 +0100
@@ -543,7 +543,7 @@
             val run_prover = run_prover params auto minimize_command
           in
             if debug then
-              Output.urgent_message (label ^ ": " ^
+              Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^
                   (if null facts then
                      "Found no relevant facts."
                    else
@@ -563,10 +563,10 @@
                       |> exists fst |> rpair state
           end
       val run_atps =
-        run_provers "ATPs" full_types atp_relevance_fudge
+        run_provers "ATP" full_types atp_relevance_fudge
                     (Translated o translate_fact ctxt) atps
       val run_smts =
-        run_provers "SMT" true smt_relevance_fudge Untranslated smts
+        run_provers "SMT solver" true smt_relevance_fudge Untranslated smts
       fun run_atps_and_smt_solvers () =
         [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
     in