--- a/src/Pure/Concurrent/lazy.ML Tue Aug 23 15:48:41 2011 +0200
+++ b/src/Pure/Concurrent/lazy.ML Tue Aug 23 16:39:21 2011 +0200
@@ -11,7 +11,6 @@
type 'a lazy
val peek: 'a lazy -> 'a Exn.result option
val is_finished: 'a lazy -> bool
- val get_finished: 'a lazy -> 'a
val lazy: (unit -> 'a) -> 'a lazy
val value: 'a -> 'a lazy
val force_result: 'a lazy -> 'a Exn.result
@@ -42,11 +41,6 @@
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 *)