--- 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, []))