diff -r 982e082cd2ba -r 85f5d7da4ab6 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -39,22 +39,11 @@
   let
     val ctxt = ctxt |> Config.put show_markup true
     val assms = op @ assmsp
-    val time = "[" ^ string_of_play_outcome result ^ "]" |> Pretty.str
-    val nr_of_assms = length assms
-    val assms = assms
-      |> map (Display.pretty_thm ctxt)
-      |> (fn [] => Pretty.str ""
-           | [a] => a
-           | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms)  (* Syntax.pretty_term!? *)
-    val concl = concl |> Syntax.pretty_term ctxt
-    val trace_list = []
-      |> cons concl
-      |> nr_of_assms > 0 ? cons (Pretty.str "\<Longrightarrow>")
-      |> cons assms
-      |> cons time
-    val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list)
+    val time = Pretty.str ("[" ^ string_of_play_outcome result ^ "]")
+    val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms)
+    val concl = Syntax.pretty_term ctxt concl
   in
-    tracing (Pretty.string_of pretty_trace)
+    tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl])))
   end
 
 fun take_time timeout tac arg =