| changeset 64570 | a2e7862e7dd5 |
| parent 64568 | a504a3dec35a |
| child 64571 | 07bbdb2079db |
--- 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 *)