# HG changeset patch
# User paulson
# Date 849087849 -3600
# Node ID cc5ee79ea4165c6759caf14d645ed36828c0da40
# Parent  a8c074224e1168684a649058e4c96d66cde4209f
Removed an obsolete and incompatible declaration

diff -r a8c074224e11 -r cc5ee79ea416 src/Pure/NJ.ML
--- 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() = ();