# HG changeset patch
# User wenzelm
# Date 1243891682 -7200
# Node ID c8821a6297f9804cb0fe6db3d50a01b97bcdf3ca
# Parent  0d3aa0aeb96ff72f9febc30fd925e75bcad20067
tuned comments;

diff -r 0d3aa0aeb96f -r c8821a6297f9 src/Pure/ML-Systems/compiler_polyml-5.0.ML
--- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Mon Jun 01 16:12:42 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Mon Jun 01 23:28:02 2009 +0200
@@ -1,6 +1,6 @@
 (*  Title:      Pure/ML-Systems/compiler_polyml-5.0.ML
 
-Runtime compilation -- for PolyML.compilerEx in version 5.0 and 5.1.
+Runtime compilation for Poly/ML 5.0 and 5.1.
 *)
 
 fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =