src/Pure/thm.ML

--- a/src/Pure/thm.ML	Tue Jan 27 00:29:37 2009 +0100
+++ b/src/Pure/thm.ML	Tue Jan 27 00:42:12 2009 +0100
@@ -1658,7 +1658,7 @@
     val {thy_ref, hyps, prop, tpairs, ...} = args;
     val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
 
-    val ps = Lazy.lazy (fn () => map (apsnd (proof_of o Future.join)) promises);
+    val ps = map (apsnd (Future.map proof_of)) promises;
     val thy = Theory.deref thy_ref;
     val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;