src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Thu Mar 17 10:22:50 2016 +0100
+++ b/src/Pure/ROOT.ML	Thu Mar 17 10:54:28 2016 +0100
@@ -34,14 +34,9 @@
 
 (* pervasive environment *)
 
-val _ = ML_Name_Space.forget_val "isSome";
-val _ = ML_Name_Space.forget_val "getOpt";
-val _ = ML_Name_Space.forget_val "valOf";
-val _ = ML_Name_Space.forget_val "foldl";
-val _ = ML_Name_Space.forget_val "foldr";
-val _ = ML_Name_Space.forget_val "print";
-val _ = ML_Name_Space.forget_val "explode";
-val _ = ML_Name_Space.forget_val "concat";
+val _ =
+  List.app ML_Name_Space.forget_val
+    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
 
 val ord = SML90.ord;
 val chr = SML90.chr;
@@ -165,6 +160,8 @@
 use "General/sha1_polyml.ML";
 use "General/sha1_samples.ML";
 
+val _ = List.app ML_Name_Space.forget_structure ML_Name_Space.critical_structures;
+
 use "PIDE/yxml.ML";
 use "PIDE/document_id.ML";