author | paulson |
Wed, 27 Nov 1996 10:44:09 +0100 | |
changeset 2241 | cc5ee79ea416 |
parent 2240 | a8c074224e11 |
child 2242 | fa8c6c695a97 |
src/Pure/NJ.ML | file | annotate | diff | comparison | revisions |
--- 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() = ();