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