--- 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