SML90 stuff;
authorwenzelm
Fri, 22 Dec 2000 18:25:00 +0100
changeset 10730bbaa0c6ef59f
parent 10729 1b3350c4ee92
child 10731 f44ab3108202
SML90 stuff;
src/Pure/ML-Systems/mlworks.ML
     1.1 --- a/src/Pure/ML-Systems/mlworks.ML	Fri Dec 22 18:24:39 2000 +0100
     1.2 +++ b/src/Pure/ML-Systems/mlworks.ML	Fri Dec 22 18:25:00 2000 +0100
     1.3 @@ -10,10 +10,10 @@
     1.4  
     1.5  (* restore old-style character / string functions *)
     1.6  
     1.7 -fun ord s = Char.ord (String.sub (s, 0));
     1.8 -val chr = str o Char.chr;
     1.9 -val explode = (map str) o String.explode;
    1.10 -val implode = String.concat;
    1.11 +val ord = SML90.ord;
    1.12 +val chr = SML90.chr;
    1.13 +val explode = SML90.explode;
    1.14 +val implode = SML90.implode;
    1.15  
    1.16  
    1.17  (* MLWorks parameters *)