# HG changeset patch
# User blanchet
# Date 1357421493 -3600
# Node ID d3111134973d1e00813b0e5fdd184921ecb1c20a
# Parent  518f0b5ef3d90d395a128b3af290459a71b7d7a6
tuned message

diff -r 518f0b5ef3d9 -r d3111134973d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jan 05 22:31:32 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jan 05 22:31:33 2013 +0100
@@ -866,7 +866,7 @@
         " proofs to learn." ^
         (if auto_level = 0 andalso not run_prover then
            "\n\nHint: Try " ^ sendback learn_proverN ^
-           " to learn from automatic provers."
+           " to learn from an automatic prover."
          else
            "")
       else