src/Pure/ROOT.ML
changeset 62659 bb29cc00c31f
parent 62658 c27dabf438d6
child 62661 c23ff2f45a18
equal deleted inserted replaced
62658:c27dabf438d6 62659:bb29cc00c31f
    32 val _ = ML_Name_Space.forget_type "ref";
    32 val _ = ML_Name_Space.forget_type "ref";
    33 
    33 
    34 
    34 
    35 (* pervasive environment *)
    35 (* pervasive environment *)
    36 
    36 
    37 val _ = ML_Name_Space.forget_val "isSome";
    37 val _ =
    38 val _ = ML_Name_Space.forget_val "getOpt";
    38   List.app ML_Name_Space.forget_val
    39 val _ = ML_Name_Space.forget_val "valOf";
    39     ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
    40 val _ = ML_Name_Space.forget_val "foldl";
       
    41 val _ = ML_Name_Space.forget_val "foldr";
       
    42 val _ = ML_Name_Space.forget_val "print";
       
    43 val _ = ML_Name_Space.forget_val "explode";
       
    44 val _ = ML_Name_Space.forget_val "concat";
       
    45 
    40 
    46 val ord = SML90.ord;
    41 val ord = SML90.ord;
    47 val chr = SML90.chr;
    42 val chr = SML90.chr;
    48 val raw_explode = SML90.explode;
    43 val raw_explode = SML90.explode;
    49 val implode = SML90.implode;
    44 val implode = SML90.implode;
   162 use "General/timing.ML";
   157 use "General/timing.ML";
   163 
   158 
   164 use "General/sha1.ML";
   159 use "General/sha1.ML";
   165 use "General/sha1_polyml.ML";
   160 use "General/sha1_polyml.ML";
   166 use "General/sha1_samples.ML";
   161 use "General/sha1_samples.ML";
       
   162 
       
   163 val _ = List.app ML_Name_Space.forget_structure ML_Name_Space.critical_structures;
   167 
   164 
   168 use "PIDE/yxml.ML";
   165 use "PIDE/yxml.ML";
   169 use "PIDE/document_id.ML";
   166 use "PIDE/document_id.ML";
   170 
   167 
   171 use "General/change_table.ML";
   168 use "General/change_table.ML";