src/Pure/ML-Systems/smlnj.ML
changeset 10725 ea048ad15283
parent 7890 0aa16bc2abdb
child 10914 aded4ba99b88
equal deleted inserted replaced
10724:819ee80305a8 10725:ea048ad15283
     7 
     7 
     8 (** ML system related **)
     8 (** ML system related **)
     9 
     9 
    10 (* restore old-style character / string functions *)
    10 (* restore old-style character / string functions *)
    11 
    11 
    12 fun ord s = Char.ord (String.sub (s, 0));
    12 val ord     = SML90.ord;
    13 val chr = str o Char.chr;
    13 val chr     = SML90.chr;
    14 val explode = (map str) o String.explode;
    14 val explode = SML90.explode;
    15 val implode = String.concat;
    15 val implode = SML90.implode;
    16 
    16 
    17 
    17 
    18 (* New Jersey ML parameters *)
    18 (* New Jersey ML parameters *)
    19 
    19 
    20 val _ =
    20 val _ =