tuned comment;

--- a/src/Pure/General/print_mode.ML	Fri Sep 03 18:03:48 2010 +0200
+++ b/src/Pure/General/print_mode.ML	Fri Sep 03 20:39:38 2010 +0200
@@ -3,6 +3,8 @@
 
 Generic print mode as thread-local value derived from global template;
 provides implicit configuration for various output mechanisms.
+
+The special print mode "input" is never enabled for output.
 *)
 
 signature BASIC_PRINT_MODE =