src/Pure/ML-Systems/smlnj.ML
changeset 10725 ea048ad15283
parent 7890 0aa16bc2abdb
child 10914 aded4ba99b88
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Thu Dec 21 19:19:18 2000 +0100
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Fri Dec 22 13:53:28 2000 +0100
     1.3 @@ -9,10 +9,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  (* New Jersey ML parameters *)