# HG changeset patch
# User wenzelm
# Date 1221580885 -7200
# Node ID 6faea8ad855999d64f11a7ecb1c0d5722649cc3d
# Parent  d67ba23e0277b901a516fc158888b237297c5de3
tuned comments;

diff -r d67ba23e0277 -r 6faea8ad8559 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Tue Sep 16 18:01:24 2008 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Sep 16 18:01:25 2008 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML-Systems/polyml.ML
     ID:         $Id$
 
-Compatibility wrapper for Poly/ML (after 5.1).
+Compatibility wrapper for Poly/ML 5.2 or later.
 *)
 
 open Thread;
diff -r d67ba23e0277 -r 6faea8ad8559 src/Pure/ML-Systems/universal.ML
--- a/src/Pure/ML-Systems/universal.ML	Tue Sep 16 18:01:24 2008 +0200
+++ b/src/Pure/ML-Systems/universal.ML	Tue Sep 16 18:01:25 2008 +0200
@@ -3,7 +3,7 @@
     Author:     Makarius
 
 Universal values via tagged union.  Emulates structure Universal
-in Poly/ML 5.1.
+from Poly/ML 5.1.
 *)
 
 signature UNIVERSAL =