src/Pure/ML/ml_compiler_polyml.ML
changeset 56305 06dcec23fb8d
parent 56304 40274e4f5ebf
child 56333 38f1422ef473
--- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 17:56:13 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 18:42:53 2014 +0100
@@ -59,8 +59,8 @@
   in
     if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
     then
-      Execution.print {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1}
-        (fn _ => output ())
+      Execution.print
+        {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1} output
     else output ()
   end;