diff -r 3546dd4ade74 -r 2d9e40cfe9af src/Pure/ML/ml_statistics.ML
--- a/src/Pure/ML/ml_statistics.ML	Fri Aug 07 20:19:49 2020 +0200
+++ b/src/Pure/ML/ml_statistics.ML	Fri Aug 07 20:28:53 2020 +0200
@@ -132,6 +132,22 @@
 
 (* 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 () =