changeset 40627 | becf5d5187cc |
parent 40393 | 2bb7ec08574a |
child 40748 | 591b6778d076 |
--- a/src/Pure/ML-Systems/smlnj.ML Fri Nov 19 23:48:07 2010 +0100 +++ b/src/Pure/ML-Systems/smlnj.ML Sat Nov 20 00:53:26 2010 +0100 @@ -30,9 +30,9 @@ (* restore old-style character / string functions *) -val ord = mk_int o SML90.ord; -val chr = SML90.chr o dest_int; -val explode = SML90.explode; +val ord = mk_int o SML90.ord; +val chr = SML90.chr o dest_int; +val raw_explode = SML90.explode; val implode = SML90.implode;