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;