| changeset 33722 | e588744f14da |
| parent 33697 | 7d6793ce0a26 |
| child 33832 | cff42395c246 |
--- a/src/Pure/thm.ML Mon Nov 16 21:56:32 2009 +0100 +++ b/src/Pure/thm.ML Mon Nov 16 21:57:16 2009 +0100 @@ -540,7 +540,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_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));