# HG changeset patch
# User blanchet
# Date 1358109758 -3600
# Node ID e12ebcb859a7d9c333f541d93590855910cd43a4
# Parent  8fc97b8da0698e5339f98a00c2d3adf080fd9938
tuned message

diff -r 8fc97b8da069 -r e12ebcb859a7 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun Jan 13 21:14:49 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun Jan 13 21:42:38 2013 +0100
@@ -244,7 +244,7 @@
                        (if null facts then
                           "Found no relevant facts."
                         else
-                          "Including (up to) " ^ string_of_int (length facts) ^
+                          "Including " ^ string_of_int (length facts) ^
                           " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
                           (facts |> map (fst o fst) |> space_implode " ") ^ ".")
                        |> print