src/Pure/thm.ML
changeset 64570 a2e7862e7dd5
parent 64568 a504a3dec35a
child 64571 07bbdb2079db
equal deleted inserted replaced
64569:deebf3ff50e6 64570:a2e7862e7dd5
   597   in bodies end;
   597   in bodies end;
   598 
   598 
   599 val proof_body_of = singleton proof_bodies_of;
   599 val proof_body_of = singleton proof_bodies_of;
   600 val proof_of = Proofterm.proof_of o proof_body_of;
   600 val proof_of = Proofterm.proof_of o proof_body_of;
   601 
   601 
   602 val join_proofs = ignore o proof_bodies_of;
   602 val join_proofs = Proofterm.join_bodies o proof_bodies_of;
   603 
   603 
   604 
   604 
   605 (* derivation status *)
   605 (* derivation status *)
   606 
   606 
   607 fun peek_status (Thm (Deriv {promises, body}, _)) =
   607 fun peek_status (Thm (Deriv {promises, body}, _)) =