--- a/src/Pure/NJ.ML	Wed Nov 27 10:43:35 1996 +0100
+++ b/src/Pure/NJ.ML	Wed Nov 27 10:44:09 1996 +0100
@@ -20,9 +20,5 @@
 
 (** Other functions which are not specific to 0.93 or 1.xx*)
 
-(*redefine to flush its output immediately -- temporary patch suggested
-  by Kim Dam Petersen*)
-val output = fn(s, t) => (output(s, t); flush_out s);
-
 (*Dummy version of the Poly/ML function*)
 fun commit() = ();