# HG changeset patch
# User wenzelm
# Date 1614959044 -3600
# Node ID d21dbfd3d69b6b34f7869324040bbc820076f0a0
# Parent  6b104dc069de5cc6d8c4550216a368e713627783
obsolete;

diff -r 6b104dc069de -r d21dbfd3d69b src/Pure/ML/ml_init.ML
--- a/src/Pure/ML/ml_init.ML	Fri Mar 05 16:09:42 2021 +0100
+++ b/src/Pure/ML/ml_init.ML	Fri Mar 05 16:44:04 2021 +0100
@@ -33,19 +33,3 @@
     if n = 1 then String.str (String.sub (s, i))
     else String.substring (s, i, n);
 end;
-
-(* FIXME workaround for 100% CPU usage in OS.Process.sleep *)
-structure OS =
-struct
-  open OS;
-  structure Process =
-  struct
-    open Process;
-    fun sleep t =
-      let
-        open Thread;
-        val lock = Mutex.mutex ();
-        val cond = ConditionVar.conditionVar ();
-      in ConditionVar.waitUntil (cond, lock, Time.now () + t) end;
-  end;
-end;
diff -r 6b104dc069de -r d21dbfd3d69b src/Pure/ML/ml_statistics.ML
--- a/src/Pure/ML/ml_statistics.ML	Fri Mar 05 16:09:42 2021 +0100
+++ b/src/Pure/ML/ml_statistics.ML	Fri Mar 05 16:44:04 2021 +0100
@@ -141,22 +141,6 @@
 
 (* monitor process *)
 
-(* FIXME workaround for 100% CPU usage in OS.Process.sleep *)
-structure OS =
-struct
-  open OS;
-  structure Process =
-  struct
-    open Process;
-    fun sleep t =
-      let
-        open Thread;
-        val lock = Mutex.mutex ();
-        val cond = ConditionVar.conditionVar ();
-      in ConditionVar.waitUntil (cond, lock, Time.now () + t) end;
-  end;
-end;
-
 fun monitor pid delay =
   let
     fun loop () =