# HG changeset patch
# User wenzelm
# Date 1350559609 -7200
# Node ID 904b7d3bde5ef3b8ca00472eb741e80c70bf517e
# Parent  8a23e8a6bc025f039925e6d91fe29f622a5b4d53
tuned message;

diff -r 8a23e8a6bc02 -r 904b7d3bde5e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Oct 18 12:47:30 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Oct 18 13:26:49 2012 +0200
@@ -339,8 +339,10 @@
 fun pretty_facts _ _ NONE = []
   | pretty_facts s ctxt (SOME ths) =
       [(Pretty.block o Pretty.fbreaks)
-        (Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"] ::
-          map (Display.pretty_thm ctxt) ths), Pretty.str ""];
+        ((if s = "" then Pretty.str "this:"
+          else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"]) ::
+          map (Display.pretty_thm ctxt) ths),
+        Pretty.str ""];
 
 fun pretty_state nr state =
   let
@@ -349,7 +351,7 @@
 
     fun prt_goal (SOME (_, (_,
       {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
-          pretty_facts "using " ctxt
+          pretty_facts "using" ctxt
             (if mode <> Backward orelse null using then NONE else SOME using) @
           [Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @
           (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
@@ -366,7 +368,7 @@
     (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
     (if verbose orelse mode = Forward then
        pretty_facts "" ctxt facts @ prt_goal (try find_goal state)
-     else if mode = Chain then pretty_facts "picking " ctxt facts
+     else if mode = Chain then pretty_facts "picking" ctxt facts
      else prt_goal (try find_goal state))
   end;