src/Pure/ML-Systems/compiler_polyml.ML
changeset 50910 54f06ba192ef
parent 47980 c81801f881b3
child 56435 28b34e8e4a80
     1.1 --- a/src/Pure/ML-Systems/compiler_polyml.ML	Wed Jan 16 11:25:26 2013 +0100
     1.2 +++ b/src/Pure/ML-Systems/compiler_polyml.ML	Wed Jan 16 11:31:08 2013 +0100
     1.3 @@ -1,8 +1,6 @@
     1.4  (*  Title:      Pure/ML-Systems/compiler_polyml.ML
     1.5  
     1.6 -Runtime compilation for Poly/ML 5.3.0 or later.
     1.7 -
     1.8 -See also Pure/ML/ml_compiler_polyml.ML for advanced version.
     1.9 +Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
    1.10  *)
    1.11  
    1.12  local