Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);
authorwenzelm
Thu, 15 Dec 2016 15:08:18 +0100
changeset 64570 a2e7862e7dd5
parent 64569 deebf3ff50e6
child 64571 07bbdb2079db
back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle