src/Pure/ML-Systems/smlnj.ML
changeset 40627 becf5d5187cc
parent 40393 2bb7ec08574a
child 40748 591b6778d076
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -30,9 +30,9 @@
     1.4  
     1.5  (* restore old-style character / string functions *)
     1.6  
     1.7 -val ord     = mk_int o SML90.ord;
     1.8 -val chr     = SML90.chr o dest_int;
     1.9 -val explode = SML90.explode;
    1.10 +val ord = mk_int o SML90.ord;
    1.11 +val chr = SML90.chr o dest_int;
    1.12 +val raw_explode = SML90.explode;
    1.13  val implode = SML90.implode;
    1.14  
    1.15