diff -r 1c8c15c30356 -r 5debc3e4fa81 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Thu Aug 23 15:44:47 2012 +0200
+++ b/src/Pure/General/file.ML	Thu Aug 23 17:46:03 2012 +0200
@@ -128,7 +128,7 @@
 (*
   scalable iterator:
   . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
-  . optional terminator at end-of-file
+  . optional terminator at end-of-input
 *)
 fun fold_chunks terminator f path a = open_input (fn file =>
   let