# HG changeset patch
# User wenzelm
# Date 1481810898 -3600
# Node ID a2e7862e7dd5ae1c12d2f660ec2aeb14faf91cad
# Parent  deebf3ff50e69bd2da6c3b3ae324395867a58881
back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);

diff -r deebf3ff50e6 -r a2e7862e7dd5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Dec 14 18:37:54 2016 +0100
+++ b/src/Pure/thm.ML	Thu Dec 15 15:08:18 2016 +0100
@@ -599,7 +599,7 @@
 val proof_body_of = singleton proof_bodies_of;
 val proof_of = Proofterm.proof_of o proof_body_of;
 
-val join_proofs = ignore o proof_bodies_of;
+val join_proofs = Proofterm.join_bodies o proof_bodies_of;
 
 
 (* derivation status *)