diff -r ae85c5d64913 -r 5d367ceecf56 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Mon Aug 08 17:23:15 2011 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Mon Aug 08 19:59:35 2011 +0200
@@ -352,8 +352,9 @@
               (case AList.lookup (op =) prfs (a, prop) of
                 NONE =>
                   let
-                    val _ = message ("Reconstructing proof of " ^ a);
-                    val _ = message (Syntax.string_of_term_global thy prop);
+                    val _ =
+                      message ("Reconstructing proof of " ^ a ^ "\n" ^
+                        Syntax.string_of_term_global thy prop);
                     val prf' = forall_intr_vfs_prf prop
                       (reconstruct_proof thy prop (Proofterm.join_proof body));
                     val (maxidx', prfs', prf) = expand