author | wenzelm |
Fri, 22 Dec 2000 18:25:00 +0100 | |
changeset 10730 | bbaa0c6ef59f |
parent 10729 | 1b3350c4ee92 |
child 10731 | f44ab3108202 |
--- a/src/Pure/ML-Systems/mlworks.ML Fri Dec 22 18:24:39 2000 +0100 +++ b/src/Pure/ML-Systems/mlworks.ML Fri Dec 22 18:25:00 2000 +0100 @@ -10,10 +10,10 @@ (* restore old-style character / string functions *) -fun ord s = Char.ord (String.sub (s, 0)); -val chr = str o Char.chr; -val explode = (map str) o String.explode; -val implode = String.concat; +val ord = SML90.ord; +val chr = SML90.chr; +val explode = SML90.explode; +val implode = SML90.implode; (* MLWorks parameters *)