src/Pure/ML/ml_pervasive_final.ML

--- a/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 18:25:42 2016 +0200
+++ b/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 19:41:58 2016 +0200
@@ -4,10 +4,11 @@
 Pervasive ML environment: final setup.
 *)
 
-if Options.default_bool "ML_system_unsafe" then ()
+if Options.default_bool "ML_system_bootstrap" then ()
 else
- (List.app ML_Name_Space.forget_structure (remove (op =) "PolyML" ML_Name_Space.excluded_structures);
-  ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
+  (List.app ML_Name_Space.forget_structure
+    (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
+   ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
 
 structure Output: OUTPUT = Output;  (*seal system channels!*)