src/Pure/proofterm.ML
changeset 33412 4b403f72a511
parent 33317 b4534348b8fd
child 33414 934801690991
     1.1 --- a/src/Pure/proofterm.ML	Wed Nov 04 20:31:36 2009 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Wed Nov 04 21:21:05 2009 +0100
     1.3 @@ -1296,6 +1296,8 @@
     1.4        in PBody {oracles = oracles, thms = thms, proof = proof} end;
     1.5  
     1.6  fun fulfill_proof_future _ [] body = Future.value body
     1.7 +  | fulfill_proof_future thy [(i, promise)] body =
     1.8 +      Future.map (fn p => fulfill_proof thy [(i, p)] body) promise
     1.9    | fulfill_proof_future thy promises body =
    1.10        Future.fork_deps (map snd promises) (fn () =>
    1.11          fulfill_proof thy (map (apsnd Future.join) promises) body);