# HG changeset patch
# User wenzelm
# Date 1460320025 -7200
# Node ID c38c08889aa9ae3718984213cf2d43f2d8f29028
# Parent  3ee643c5ed00c1640e04f880266029d06a585baf
tuned comments;

diff -r 3ee643c5ed00 -r c38c08889aa9 src/Pure/General/socket_io.ML
--- a/src/Pure/General/socket_io.ML	Sun Apr 10 21:46:12 2016 +0200
+++ b/src/Pure/General/socket_io.ML	Sun Apr 10 22:27:05 2016 +0200
@@ -4,8 +4,6 @@
 
 Stream IO over TCP sockets.  Following example 10.2 in "The Standard
 ML Basis Library" by Emden R. Gansner and John H. Reppy.
-
-Note: BinIO requires Poly/ML 5.5.x to work reliably.
 *)
 
 signature SOCKET_IO =
diff -r 3ee643c5ed00 -r c38c08889aa9 src/Pure/ML/ml_profiling.ML
--- a/src/Pure/ML/ml_profiling.ML	Sun Apr 10 21:46:12 2016 +0200
+++ b/src/Pure/ML/ml_profiling.ML	Sun Apr 10 22:27:05 2016 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_profiling.ML
     Author:     Makarius
 
-Profiling for Poly/ML 5.6.
+ML profiling.
 *)
 
 signature ML_PROFILING =
diff -r 3ee643c5ed00 -r c38c08889aa9 src/Pure/ML/ml_statistics.ML
--- a/src/Pure/ML/ml_statistics.ML	Sun Apr 10 21:46:12 2016 +0200
+++ b/src/Pure/ML/ml_statistics.ML	Sun Apr 10 22:27:05 2016 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_statistics.ML
     Author:     Makarius
 
-ML runtime statistics for Poly/ML 5.5.0 or later.
+ML runtime statistics.
 *)
 
 signature ML_STATISTICS =