src/Pure/General/susp.ML
changeset 25317 8b38b394fa8e
parent 25310 2b928fb92f53
child 26063 b2862698dc79
--- a/src/Pure/General/susp.ML	Tue Nov 06 22:50:34 2007 +0100
+++ b/src/Pure/General/susp.ML	Tue Nov 06 22:50:35 2007 +0100
@@ -28,19 +28,15 @@
 
 fun delay f = ref (Delay f);
 
-fun force susp =
-  let
-    fun forc () = case ! susp
-     of Value v => v
+fun force (ref (Value v)) = v
+  | force susp = NAMED_CRITICAL "susp" (fn () =>
+      (case ! susp of
+        Value v => v   (*race wrt. parallel force*)
       | Delay f =>
           let
             val v = f ();
             val _ = susp := Value v;
-          in v end;
-  in case ! susp
-   of Value v => v
-    | Delay _ => NAMED_CRITICAL "sups" forc
-  end;
+          in v end));
 
 fun peek susp =
   (case ! susp of