src/Pure/ML-Systems/polyml-4.0.ML
changeset 10708 1a6348a11489
parent 10518 20d4899f5d48
child 10914 aded4ba99b88
equal deleted inserted replaced
10707:9285b4d87d7d 10708:1a6348a11489
    19 end;
    19 end;
    20 
    20 
    21 
    21 
    22 (* restore old-style character / string functions *)
    22 (* restore old-style character / string functions *)
    23 
    23 
    24 fun ord s = Char.ord (String.sub (s, 0));
    24 val ord = SML90.ord;
    25 val chr = str o Char.chr;
    25 val chr = SML90.chr;
    26 val explode = (map str) o String.explode;
    26 val explode = SML90.explode;
    27 val implode = String.concat;
    27 val implode = SML90.implode;
    28 
    28 
    29 
    29 
    30 (*Note start point for timing*)
    30 (*Note start point for timing*)
    31 fun startTiming() =
    31 fun startTiming() =
    32   let val CPUtimer = Timer.startCPUTimer();
    32   let val CPUtimer = Timer.startCPUTimer();