# HG changeset patch
# User wenzelm
# Date 1312826375 -7200
# Node ID 5d367ceecf564c9efc0d702deedce6767465d8cb
# Parent  ae85c5d64913050e7d3565634e4164af1b8eac0f
ship message in one piece;

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