src/Pure/ROOT.ML
changeset 62659 bb29cc00c31f
parent 62658 c27dabf438d6
child 62661 c23ff2f45a18
     1.1 --- a/src/Pure/ROOT.ML	Thu Mar 17 10:22:50 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Thu Mar 17 10:54:28 2016 +0100
     1.3 @@ -34,14 +34,9 @@
     1.4  
     1.5  (* pervasive environment *)
     1.6  
     1.7 -val _ = ML_Name_Space.forget_val "isSome";
     1.8 -val _ = ML_Name_Space.forget_val "getOpt";
     1.9 -val _ = ML_Name_Space.forget_val "valOf";
    1.10 -val _ = ML_Name_Space.forget_val "foldl";
    1.11 -val _ = ML_Name_Space.forget_val "foldr";
    1.12 -val _ = ML_Name_Space.forget_val "print";
    1.13 -val _ = ML_Name_Space.forget_val "explode";
    1.14 -val _ = ML_Name_Space.forget_val "concat";
    1.15 +val _ =
    1.16 +  List.app ML_Name_Space.forget_val
    1.17 +    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
    1.18  
    1.19  val ord = SML90.ord;
    1.20  val chr = SML90.chr;
    1.21 @@ -165,6 +160,8 @@
    1.22  use "General/sha1_polyml.ML";
    1.23  use "General/sha1_samples.ML";
    1.24  
    1.25 +val _ = List.app ML_Name_Space.forget_structure ML_Name_Space.critical_structures;
    1.26 +
    1.27  use "PIDE/yxml.ML";
    1.28  use "PIDE/document_id.ML";
    1.29