tuned messages;

--- a/src/Pure/Isar/proof.ML	Tue Oct 16 20:23:00 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 16 20:35:24 2012 +0200
@@ -338,7 +338,7 @@
 
 fun pretty_facts _ _ NONE = []
   | pretty_facts s ctxt (SOME ths) =
-      [Pretty.chunks
+      [(Pretty.block o Pretty.fbreaks)
         (Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"] ::
           map (Display.pretty_thm ctxt) ths), Pretty.str ""];
 

--- a/src/Pure/Isar/proof_display.ML	Tue Oct 16 20:23:00 2012 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Oct 16 20:35:24 2012 +0200
@@ -120,10 +120,9 @@
     val pr_facts =
       if null facts then ""
       else
-        Pretty.string_of
-          (Pretty.chunks
-            (Pretty.block [Pretty.command "using", Pretty.brk 1, Pretty.str "this:"] ::
-              map (Display.pretty_thm ctxt) facts)) ^ "\n";
+        (Pretty.string_of o Pretty.block o Pretty.fbreaks)
+          (Pretty.block [Pretty.command "using", Pretty.brk 1, Pretty.str "this:"] ::
+            map (Display.pretty_thm ctxt) facts) ^ "\n";
     val pr_goal = string_of_goal ctxt goal;
   in pr_header ^ pr_facts ^ pr_goal end);