diff -r 8b1969d603c0 -r 538b94dc62de src/HOL/Tools/try.ML
--- a/src/HOL/Tools/try.ML	Sat Sep 11 16:36:23 2010 +0200
+++ b/src/HOL/Tools/try.ML	Sat Sep 11 16:39:54 2010 +0200
@@ -70,6 +70,8 @@
     [] => (if auto then () else writeln "No proof found."; (false, st))
   | xs as (s, _) :: _ =>
     let
+      val xs = xs |> map swap |> AList.coalesce (op =)
+                  |> map (swap o apsnd commas)
       val message =
         (if auto then "Auto Try found a proof" else "Try this command") ^ ": " ^
         Markup.markup Markup.sendback