--- a/src/Pure/ML/ml_pervasive_final.ML Mon Apr 04 23:08:43 2016 +0200
+++ b/src/Pure/ML/ml_pervasive_final.ML Mon Apr 04 23:08:48 2016 +0200
@@ -6,9 +6,8 @@
if Options.default_bool "ML_system_unsafe" then ()
else
- (List.app ML_Name_Space.forget_structure
- ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
- ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
+ (List.app ML_Name_Space.forget_structure (remove (op =) "PolyML" ML_Name_Space.exclude_structures);
+ ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
structure Output: OUTPUT = Output; (*seal system channels!*)