src/Pure/thm.ML
changeset 44247 270366301bd7
parent 44108 476a239d3e0e
child 44303 4e2abb045eac
equal deleted inserted replaced
44246:380a4677c55d 44247:270366301bd7
   513 fun raw_body (Thm (Deriv {body, ...}, _)) = body;
   513 fun raw_body (Thm (Deriv {body, ...}, _)) = body;
   514 
   514 
   515 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
   515 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
   516   Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
   516   Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
   517     (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
   517     (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
   518 and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
   518 and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
   519 
   519 
   520 val join_proofs = Proofterm.join_bodies o map fulfill_body;
   520 val join_proofs = Proofterm.join_bodies o map fulfill_body;
   521 
   521 
   522 fun proof_body_of thm = (Proofterm.join_bodies [raw_body thm]; fulfill_body thm);
   522 fun proof_body_of thm = (Proofterm.join_bodies [raw_body thm]; fulfill_body thm);
   523 val proof_of = Proofterm.proof_of o proof_body_of;
   523 val proof_of = Proofterm.proof_of o proof_body_of;