# HG changeset patch
# User wenzelm
# Date 1358332268 -3600
# Node ID 54f06ba192efc5acb76571e1e96c787a56440a14
# Parent  b2fb1ab1475dbd30b60e2acfc7575307862fa65c
tuned comments;

diff -r b2fb1ab1475d -r 54f06ba192ef src/Pure/ML-Systems/compiler_polyml.ML
--- a/src/Pure/ML-Systems/compiler_polyml.ML	Wed Jan 16 11:25:26 2013 +0100
+++ b/src/Pure/ML-Systems/compiler_polyml.ML	Wed Jan 16 11:31:08 2013 +0100
@@ -1,8 +1,6 @@
 (*  Title:      Pure/ML-Systems/compiler_polyml.ML
 
-Runtime compilation for Poly/ML 5.3.0 or later.
-
-See also Pure/ML/ml_compiler_polyml.ML for advanced version.
+Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
 *)
 
 local
diff -r b2fb1ab1475d -r 54f06ba192ef src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jan 16 11:25:26 2013 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jan 16 11:31:08 2013 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML-Systems/multithreading_polyml.ML
     Author:     Makarius
 
-Multithreading in Poly/ML 5.3.0 or later (cf. polyml/basis/Thread.sml).
+Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
 *)
 
 signature MULTITHREADING_POLYML =
diff -r b2fb1ab1475d -r 54f06ba192ef src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Wed Jan 16 11:25:26 2013 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Jan 16 11:31:08 2013 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML-Systems/polyml.ML
     Author:     Makarius
 
-Compatibility wrapper for Poly/ML 5.3.0 or later.
+Compatibility wrapper for Poly/ML.
 *)
 
 (* exceptions *)
diff -r b2fb1ab1475d -r 54f06ba192ef src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Wed Jan 16 11:25:26 2013 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Jan 16 11:31:08 2013 +0100
@@ -1,6 +1,6 @@
 (*  Title:      Pure/ML-Systems/smlnj.ML
 
-Compatibility file for Standard ML of New Jersey 110 or later.
+Compatibility file for Standard ML of New Jersey.
 *)
 
 use "ML-Systems/proper_int.ML";
diff -r b2fb1ab1475d -r 54f06ba192ef src/Pure/ML/install_pp_polyml.ML
--- a/src/Pure/ML/install_pp_polyml.ML	Wed Jan 16 11:25:26 2013 +0100
+++ b/src/Pure/ML/install_pp_polyml.ML	Wed Jan 16 11:31:08 2013 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/install_pp_polyml.ML
     Author:     Makarius
 
-Extra toplevel pretty-printing for Poly/ML 5.3.0 or later.
+Extra toplevel pretty-printing for Poly/ML.
 *)
 
 PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
diff -r b2fb1ab1475d -r 54f06ba192ef src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Jan 16 11:25:26 2013 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Jan 16 11:31:08 2013 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_compiler_polyml.ML
     Author:     Makarius
 
-Advanced runtime compilation for Poly/ML 5.3.0 or later.
+Advanced runtime compilation for Poly/ML.
 *)
 
 structure ML_Compiler: ML_COMPILER =