src/Pure/thm.ML
changeset 44303 4e2abb045eac
parent 44247 270366301bd7
child 44330 b28e091f683a
     1.1 --- a/src/Pure/thm.ML	Fri Aug 19 18:01:23 2011 +0200
     1.2 +++ b/src/Pure/thm.ML	Fri Aug 19 21:40:52 2011 +0200
     1.3 @@ -517,9 +517,9 @@
     1.4      (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
     1.5  and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
     1.6  
     1.7 -val join_proofs = Proofterm.join_bodies o map fulfill_body;
     1.8 +fun join_proofs thms = ignore (map fulfill_body thms);
     1.9  
    1.10 -fun proof_body_of thm = (Proofterm.join_bodies [raw_body thm]; fulfill_body thm);
    1.11 +fun proof_body_of thm = (Proofterm.join_body (raw_body thm); fulfill_body thm);
    1.12  val proof_of = Proofterm.proof_of o proof_body_of;
    1.13  
    1.14