# HG changeset patch
# User wenzelm
# Date 1459873116 -7200
# Node ID bf1b4d3440a3692c0760444f1fd1d510f815a6a2
# Parent  4a6cbe1239fe7d4f0d1178d6726e45a66aad1d7b
tuned;

diff -r 4a6cbe1239fe -r bf1b4d3440a3 src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Tue Apr 05 18:16:11 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Tue Apr 05 18:18:36 2016 +0200
@@ -60,13 +60,15 @@
 
   (* Standard ML name space *)
 
-  val exclude_structures = ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
+  val excluded_values = ["use", "exit"];
+  val excluded_structures = ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
 
-  val sml_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
+  val sml_val =
+    List.filter (fn (a, _) => List.all (fn b => a <> b) excluded_values) (#allVal global ());
   val sml_type = #allType global ();
   val sml_fixity = #allFix global ();
   val sml_structure =
-    List.filter (fn (a, _) => List.all (fn b => a <> b) exclude_structures) (#allStruct global ());
+    List.filter (fn (a, _) => List.all (fn b => a <> b) excluded_structures) (#allStruct global ());
   val sml_signature = #allSig global ();
   val sml_functor = #allFunct global ();
 end;
diff -r 4a6cbe1239fe -r bf1b4d3440a3 src/Pure/ML/ml_pervasive_final.ML
--- a/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 18:16:11 2016 +0200
+++ b/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 18:18:36 2016 +0200
@@ -6,7 +6,7 @@
 
 if Options.default_bool "ML_system_unsafe" then ()
 else
- (List.app ML_Name_Space.forget_structure (remove (op =) "PolyML" ML_Name_Space.exclude_structures);
+ (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>);
 
 structure Output: OUTPUT = Output;  (*seal system channels!*)