# HG changeset patch
# User wenzelm
# Date 1187293928 -7200
# Node ID 91d8937992127fdad4b4c476b0caed4406ae2b53
# Parent  229fdfc1ddd97bec70a31d79bf5645c65746cfbf
force: non-critical, but also non-thread-safe (potentially multiple evaluations);

diff -r 229fdfc1ddd9 -r 91d893799212 src/Pure/General/susp.ML
--- a/src/Pure/General/susp.ML	Thu Aug 16 21:52:07 2007 +0200
+++ b/src/Pure/General/susp.ML	Thu Aug 16 21:52:08 2007 +0200
@@ -2,7 +2,8 @@
     ID:         $Id$
     Author:     Sebastian Skalberg and Florian Haftmann, TU Muenchen
 
-Delayed evaluation.
+Delayed evaluation. Supposed to be value oriented; may result in
+multiple evaluations in a multi-threaded environment!
 *)
 
 signature SUSP =
@@ -28,14 +29,14 @@
 
 fun delay f = ref (Delay f);
 
-fun force susp = NAMED_CRITICAL "susp" (fn () =>
+fun force susp =
   (case ! susp of
     Value v => v
   | Delay f =>
       let
         val v = f ();
         val _ = susp := Value v;
-      in v end));
+      in v end);
 
 fun peek susp =
   (case ! susp of
@@ -44,4 +45,4 @@
 
 fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*)
 
-end
+end;