# HG changeset patch
# User wenzelm
# Date 850726900 -3600
# Node ID 8115988ccc22745eb7039ae13444d3a972db8755
# Parent  b3d273ce5601b9a27619ec8f73592424d43a41ec
fixed comment;

diff -r b3d273ce5601 -r 8115988ccc22 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Dec 16 10:01:17 1996 +0100
+++ b/src/Pure/library.ML	Mon Dec 16 10:01:40 1996 +0100
@@ -5,7 +5,7 @@
 
 Basic library: functions, options, pairs, booleans, lists, integers,
 strings, lists as sets, association lists, generic tables, balanced trees,
-input / TextIO.output, timing, filenames, misc functions.
+input / output, timing, filenames, misc functions.
 *)
 
 infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto