src/Pure/thm.ML
changeset 32094 89b9210c7506
parent 32059 7991cdf10a54
child 32104 d1d98a02473e
     1.1 --- a/src/Pure/thm.ML	Tue Jul 21 10:23:16 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Tue Jul 21 10:24:57 2009 +0200
     1.3 @@ -1612,8 +1612,9 @@
     1.4  fun raw_body (Thm (Deriv {body, ...}, _)) = body;
     1.5  
     1.6  fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
     1.7 -  let val ps = map (apsnd (fulfill_body o Future.join)) promises
     1.8 -  in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
     1.9 +  Pt.fulfill_proof (Theory.deref thy_ref)
    1.10 +    (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
    1.11 +and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
    1.12  
    1.13  fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
    1.14  val proof_of = Pt.proof_of o proof_body_of;
    1.15 @@ -1652,7 +1653,7 @@
    1.16      val _ = null hyps orelse err "bad hyps";
    1.17      val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
    1.18      val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
    1.19 -    val _ = List.app (ignore o fulfill_body o Future.join o #2) promises;
    1.20 +    val _ = fulfill_bodies (map #2 promises);
    1.21    in thm end;
    1.22  
    1.23  fun future future_thm ct =