src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
changeset 50866 e12ebcb859a7
parent 50749 82dee320d340
child 50876 e6317e8b11db
--- 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