src/Pure/Concurrent/lazy_sequential.ML

--- a/src/Pure/Concurrent/lazy_sequential.ML	Tue Aug 23 12:20:12 2011 +0200
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Tue Aug 23 15:48:41 2011 +0200
@@ -45,6 +45,14 @@
   in result end;
 
 fun force r = Exn.release (force_result r);
+fun map f x = lazy (fn () => f (force x));
+
+
+(* future evaluation *)
+
+fun future params x =
+  if is_finished x then Future.value_result (force_result x)
+  else (singleton o Future.forks) params (fn () => force x);
 
 end;
 end;