A definition of "print", unfortunately overridden by each "open PolyML"

--- a/src/Pure/basis.ML	Fri Jan 03 15:01:55 1997 +0100
+++ b/src/Pure/basis.ML	Fri Jan 03 15:25:51 1997 +0100
@@ -100,3 +100,6 @@
   val output 	= output
   val flushOut 	= flush_out
   end;
+
+
+fun print s = (output (std_out, s); flush_out std_out);