src/Pure/ML-Systems/polyml_common.ML
changeset 40627 becf5d5187cc
parent 40393 2bb7ec08574a
child 40748 591b6778d076
     1.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -29,6 +29,7 @@
     1.4  val _ = PolyML.Compiler.forgetValue "foldl";
     1.5  val _ = PolyML.Compiler.forgetValue "foldr";
     1.6  val _ = PolyML.Compiler.forgetValue "print";
     1.7 +val _ = PolyML.Compiler.forgetValue "explode";
     1.8  
     1.9  
    1.10  (* Compiler options *)
    1.11 @@ -48,7 +49,7 @@
    1.12  
    1.13  val ord = SML90.ord;
    1.14  val chr = SML90.chr;
    1.15 -val explode = SML90.explode;
    1.16 +val raw_explode = SML90.explode;
    1.17  val implode = SML90.implode;
    1.18  
    1.19