--- 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
--- 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 =
--- 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 *)
--- 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";
--- 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 =>
--- 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 =