src/Pure/Concurrent/lazy_sequential.ML

--- a/src/Pure/Concurrent/lazy_sequential.ML	Mon Aug 15 16:38:42 2011 +0200
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Mon Aug 15 19:27:55 2011 +0200
@@ -25,6 +25,13 @@
 fun lazy e = Lazy (Unsynchronized.ref (Expr e));
 fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a)));
 
+fun is_finished x = is_some (peek x);
+
+fun get_finished x =
+  (case peek x of
+    SOME res => Exn.release res
+  | NONE => raise Fail "Unfinished lazy evaluation");
+
 
 (* force result *)