# HG changeset patch
# User blanchet
# Date 1284042748 -7200
# Node ID 17bce41f175f9c1770c6c9dfb289caab78d53b49
# Parent  e2a3c435334bd04630acb76f9f635fda877e8d16
tuning

diff -r e2a3c435334b -r 17bce41f175f src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Sep 09 16:27:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Sep 09 16:32:28 2010 +0200
@@ -91,12 +91,11 @@
     val bracket =
       implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg)
                                ^ "]") args)
-    val space_bracket = if bracket = "" then "" else " " ^ bracket
     val name =
       case xref of
-        Facts.Fact s => "`" ^ s ^ "`" ^ space_bracket
+        Facts.Fact s => "`" ^ s ^ "`" ^ bracket
       | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
-      | _ => Facts.string_of_ref xref ^ space_bracket
+      | _ => Facts.string_of_ref xref ^ bracket
     val multi = length ths > 1
   in
     (ths, (1, []))