src/Pure/ML/ml_name_space.ML
changeset 62860 045dc4ad6d98
parent 62853 8e54fd480809
child 62872 bf1b4d3440a3
--- a/src/Pure/ML/ml_name_space.ML	Mon Apr 04 23:08:43 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Mon Apr 04 23:08:48 2016 +0200
@@ -60,14 +60,13 @@
 
   (* Standard ML name space *)
 
+  val exclude_structures = ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
+
   val sml_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#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)
-        ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"])
-      (#allStruct global ());
+    List.filter (fn (a, _) => List.all (fn b => a <> b) exclude_structures) (#allStruct global ());
   val sml_signature = #allSig global ();
   val sml_functor = #allFunct global ();
 end;