changeset 32726 | a900d3cd47cc |
parent 32725 | 57e29093ecfb |
child 32784 | 1a5dde5079ac |
--- a/src/Pure/thm.ML Mon Sep 28 12:09:55 2009 +0200 +++ b/src/Pure/thm.ML Mon Sep 28 20:52:05 2009 +0200 @@ -541,7 +541,7 @@ fun raw_body (Thm (Deriv {body, ...}, _)) = body; fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) = - Pt.fulfill_proof (Theory.deref thy_ref) + Pt.fulfill_proof (Theory.deref thy_ref) ~1 (map #1 promises ~~ fulfill_bodies (map #2 promises)) body and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));