src/Pure/ROOT.ML
changeset 62657 cdd6db02eae8
parent 62643 6f7ac44365d7
child 62658 c27dabf438d6
     1.1 --- a/src/Pure/ROOT.ML	Thu Mar 17 10:00:38 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Thu Mar 17 10:21:43 2016 +0100
     1.3 @@ -28,20 +28,20 @@
     1.4  use "Concurrent/multithreading.ML";
     1.5  
     1.6  use "Concurrent/unsynchronized.ML";
     1.7 -val _ = PolyML.Compiler.forgetValue "ref";
     1.8 -val _ = PolyML.Compiler.forgetType "ref";
     1.9 +val _ = ML_Name_Space.forget_val "ref";
    1.10 +val _ = ML_Name_Space.forget_type "ref";
    1.11  
    1.12  
    1.13  (* pervasive environment *)
    1.14  
    1.15 -val _ = PolyML.Compiler.forgetValue "isSome";
    1.16 -val _ = PolyML.Compiler.forgetValue "getOpt";
    1.17 -val _ = PolyML.Compiler.forgetValue "valOf";
    1.18 -val _ = PolyML.Compiler.forgetValue "foldl";
    1.19 -val _ = PolyML.Compiler.forgetValue "foldr";
    1.20 -val _ = PolyML.Compiler.forgetValue "print";
    1.21 -val _ = PolyML.Compiler.forgetValue "explode";
    1.22 -val _ = PolyML.Compiler.forgetValue "concat";
    1.23 +val _ = ML_Name_Space.forget_val "isSome";
    1.24 +val _ = ML_Name_Space.forget_val "getOpt";
    1.25 +val _ = ML_Name_Space.forget_val "valOf";
    1.26 +val _ = ML_Name_Space.forget_val "foldl";
    1.27 +val _ = ML_Name_Space.forget_val "foldr";
    1.28 +val _ = ML_Name_Space.forget_val "print";
    1.29 +val _ = ML_Name_Space.forget_val "explode";
    1.30 +val _ = ML_Name_Space.forget_val "concat";
    1.31  
    1.32  val ord = SML90.ord;
    1.33  val chr = SML90.chr;