| changeset 31329 | c8821a6297f9 |
| parent 31312 | 1c00e4ff3c99 |
| child 31480 | 05937d6aafb5 |
--- 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 =