clarified modules;

--- a/src/Pure/ML/ml_final.ML	Mon Apr 04 20:07:08 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      Pure/ML/ml_final.ML
-    Author:     Makarius
-
-Final setup of ML environment.
-*)
-
-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>);
-
-structure Output: OUTPUT = Output;  (*seal system channels!*)
-
-structure Pure = struct val thy = Thy_Info.pure_theory () end;
-
-Proofterm.proofs := 0;
-
-Context.set_thread_data NONE;

--- a/src/Pure/ML/ml_pervasive.ML	Mon Apr 04 20:07:08 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(*  Title:      Pure/ML/ml_pervasive.ML
-    Author:     Makarius
-
-Pervasive ML environment.
-*)
-
-structure PolyML_Pretty =
-struct
-  datatype context = datatype PolyML.context;
-  datatype pretty = datatype PolyML.pretty;
-end;
-
-val seconds = Time.fromReal;
-
-val _ =
-  List.app ML_Name_Space.forget_val
-    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
-
-val ord = SML90.ord;
-val chr = SML90.chr;
-val raw_explode = SML90.explode;
-val implode = SML90.implode;
-
-val pointer_eq = PolyML.pointerEq;
-
-val error_depth = PolyML.error_depth;
-
-open Thread;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_pervasive_final.ML	Mon Apr 04 20:20:47 2016 +0200
@@ -0,0 +1,19 @@
+(*  Title:      Pure/ML/ml_pervasive_final.ML
+    Author:     Makarius
+
+Pervasive ML environment: final setup.
+*)
+
+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>);
+
+structure Output: OUTPUT = Output;  (*seal system channels!*)
+
+structure Pure = struct val thy = Thy_Info.pure_theory () end;
+
+Proofterm.proofs := 0;
+
+Context.set_thread_data NONE;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_pervasive_initial.ML	Mon Apr 04 20:20:47 2016 +0200
@@ -0,0 +1,28 @@
+(*  Title:      Pure/ML/ml_pervasive_initial.ML
+    Author:     Makarius
+
+Pervasive ML environment: initial setup.
+*)
+
+structure PolyML_Pretty =
+struct
+  datatype context = datatype PolyML.context;
+  datatype pretty = datatype PolyML.pretty;
+end;
+
+val seconds = Time.fromReal;
+
+val _ =
+  List.app ML_Name_Space.forget_val
+    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
+
+val ord = SML90.ord;
+val chr = SML90.chr;
+val raw_explode = SML90.explode;
+val implode = SML90.implode;
+
+val pointer_eq = PolyML.pointerEq;
+
+val error_depth = PolyML.error_depth;
+
+open Thread;

--- a/src/Pure/ROOT	Mon Apr 04 20:07:08 2016 +0200
+++ b/src/Pure/ROOT	Mon Apr 04 20:20:47 2016 +0200
@@ -108,12 +108,12 @@
     "ML/ml_context.ML"
     "ML/ml_debugger.ML"
     "ML/ml_env.ML"
-    "ML/ml_final.ML"
     "ML/ml_heap.ML"
     "ML/ml_lex.ML"
     "ML/ml_name_space.ML"
     "ML/ml_options.ML"
-    "ML/ml_pervasive.ML"
+    "ML/ml_pervasive_final.ML"
+    "ML/ml_pervasive_initial.ML"
     "ML/ml_pp.ML"
     "ML/ml_pretty.ML"
     "ML/ml_profiling.ML"

--- a/src/Pure/ROOT.ML	Mon Apr 04 20:07:08 2016 +0200
+++ b/src/Pure/ROOT.ML	Mon Apr 04 20:20:47 2016 +0200
@@ -6,7 +6,7 @@
 
 use "ML/ml_system.ML";
 use "ML/ml_name_space.ML";
-use "ML/ml_pervasive.ML";
+use "ML/ml_pervasive_initial.ML";
 
 if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
 else use "ML/fixed_int_dummy.ML";
@@ -338,7 +338,4 @@
 
 use_thy "Pure";
 
-
-(* final ML setup *)
-
-use "ML/ml_final.ML";
+use "ML/ml_pervasive_final.ML";