src/Pure/ML/ml_name_space.ML
changeset 62930 51ac6bc389e8
parent 62929 b92565f98206
child 62934 6e3fb0aa857a
     1.1 --- a/src/Pure/ML/ml_name_space.ML	Sat Apr 09 14:52:10 2016 +0200
     1.2 +++ b/src/Pure/ML/ml_name_space.ML	Sat Apr 09 16:16:05 2016 +0200
     1.3 @@ -65,10 +65,11 @@
     1.4        "chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
     1.5    val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
     1.6    val bootstrap_structures =
     1.7 -    ["Exn", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive", "PolyML"] @
     1.8 -      hidden_structures;
     1.9 +    ["Exn", "Output_Primitives", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive",
    1.10 +      "Private_Output", "PolyML"] @ hidden_structures;
    1.11    val bootstrap_signatures =
    1.12 -    ["EXN", "BASIC_EXN", "THREAD_DATA", "THREAD_POSITION", "ML_RECURSIVE"];
    1.13 +    ["EXN", "OUTPUT_PRIMITIVES", "BASIC_EXN", "THREAD_DATA", "THREAD_POSITION", "ML_RECURSIVE",
    1.14 +      "PRIVATE_OUTPUT"];
    1.15  
    1.16  
    1.17    (* Standard ML environment *)