diff -r 2183c731f0a7 -r 8a6788917b32 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Sun Jan 11 12:46:19 2015 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Sun Jan 11 13:12:47 2015 +0100
@@ -14,7 +14,6 @@
   val peek: 'a lazy -> 'a Exn.result option
   val is_running: 'a lazy -> bool
   val is_finished: 'a lazy -> bool
-  val finished_result: 'a lazy -> 'a Exn.result option
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
   val map: ('a -> 'b) -> 'a lazy -> 'b lazy
@@ -55,15 +54,6 @@
   is_future (fn res =>
     Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))) x;
 
-fun finished_result (Lazy var) =
-  (case Synchronized.value var of
-    Expr _ => NONE
-  | Result res =>
-      if Future.is_finished res then
-        let val result = Future.join_result res
-        in if Exn.is_interrupt_exn result then NONE else SOME result end
-      else NONE);
-
 
 (* force result *)