--- a/src/Pure/ML/ml_compiler.ML Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/ML/ml_compiler.ML Wed May 09 20:45:57 2018 +0200
@@ -120,7 +120,7 @@
|> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
|> Output.report;
val _ =
- if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
+ if not (null persistent_reports) andalso redirect andalso Future.enabled ()
then
Execution.print
{name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}