Flush stdout after outputting debug message

TextIO.output() doesn't flush stdout, but print() does. Flushing is
necessary to make sure the messages are printed in a timely fashion,
which is important when debugging timing/performance issues.

The performance hit of the extra flushing should be negligible, as
even when these debug messages are enabled, they are only printed a
few dozen times or so.

tools-poly/poly/poly-init2.ML

@@ -32,7 +32,7 @@ local
   val meta_debug = ref false
 
   fun MDBG s = if !meta_debug then
-                 TextIO.output(TextIO.stdOut, "META_DEBUG: " ^ s() ^ "\n")
+                 TextIO.print("META_DEBUG: " ^ s() ^ "\n")
                else ()
 
   infix ++