--- a/src/Pure/thm.ML Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/thm.ML Wed Aug 17 22:14:22 2011 +0200
@@ -515,7 +515,7 @@
fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
(map #1 promises ~~ fulfill_bodies (map #2 promises)) body
-and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
+and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
val join_proofs = Proofterm.join_bodies o map fulfill_body;