1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Mar 18 17:27:28 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Mar 18 22:55:28 2011 +0100
     1.3 @@ -115,8 +115,8 @@
     1.4    let
     1.5      val ths = Attrib.eval_thms ctxt [xthm]
     1.6      val bracket =
     1.7 -      implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg)
     1.8 -                               ^ "]") args)
     1.9 +      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
    1.10 +      |> implode
    1.11      fun nth_name j =
    1.12        case xref of
    1.13          Facts.Fact s => backquote s ^ bracket