# HG changeset patch
# User wenzelm
# Date 1535373112 -7200
# Node ID 6296915dee6e26c209b2d53e5352285a13fad2ec
# Parent  6a0b1357bded0b581e13f5e2857a8bca044539c7
tuned;

diff -r 6a0b1357bded -r 6296915dee6e src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Sun Aug 26 17:48:35 2018 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Mon Aug 27 14:31:52 2018 +0200
@@ -12,8 +12,8 @@
   val forget_val: string -> unit
   val forget_type: string -> unit
   val forget_structure: string -> unit
+  val hidden_structures: string list
   val bootstrap_values: string list
-  val hidden_structures: string list
   val bootstrap_structures: string list
   val bootstrap_signatures: string list
   val sml_val: (string * PolyML.NameSpace.Values.value) list
@@ -64,13 +64,14 @@
 val forget_type = PolyML.Compiler.forgetType;
 val forget_structure = PolyML.Compiler.forgetStructure;
 
+val hidden_structures = ["CInterface", "Foreign", "RunCall", "Signal"];
+
 
 (* bootstrap environment *)
 
 val bootstrap_values =
   ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload",
     "chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
-val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
 val bootstrap_structures =
   ["Exn", "Output_Primitives", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive",
     "Private_Output", "PolyML"] @ hidden_structures;