# HG changeset patch
# User blanchet
# Date 1404226030 -7200
# Node ID 3e94eb1124b070b6c7eff6c80547b9e6dec7c765
# Parent  d6df9b63d38530edca5850143fcda7f8fb35c335
tuned message

diff -r d6df9b63d385 -r 3e94eb1124b0 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 01 16:47:10 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 01 16:47:10 2014 +0200
@@ -196,8 +196,11 @@
   (facts |> map (fst o fst) |> space_implode " ") ^ "."
 
 fun string_of_factss factss =
-  if forall (null o snd) factss then "Found no relevant facts."
-  else cat_lines (map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) factss)
+  if forall (null o snd) factss then
+    "Found no relevant facts."
+  else
+    cat_lines (map (fn (filter, facts) =>
+      (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss)
 
 fun run_sledgehammer (params as {verbose, spy, blocking, provers, max_facts, ...}) mode
     output_result i (fact_override as {only, ...}) minimize_command state =