# HG changeset patch
# User wenzelm
# Date 1459778036 -7200
# Node ID 3c576c7f97313998290d62e9adbbd6783e4b7f75
# Parent  31177a9c30254cca5e3d23c1cb14d2dd420c87a9
clarified final setup of ML environment;

diff -r 31177a9c3025 -r 3c576c7f9731 src/Pure/ML/ml_final.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_final.ML	Mon Apr 04 15:53:56 2016 +0200
@@ -0,0 +1,21 @@
+(*  Title:      Pure/ML/ml_final.ML
+    Author:     Makarius
+
+Final setup of ML environment.
+*)
+
+(*no access to system internals!*)
+structure PolyML = struct structure IntInf = PolyML.IntInf end;
+val _ = List.app ML_Name_Space.forget_structure ML_Name_Space.critical_structures;
+
+structure Output: OUTPUT = Output;  (*seal system channels!*)
+
+structure Pure = struct val thy = Thy_Info.pure_theory () end;
+
+fun use_thys args =
+  Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
+val use_thy = use_thys o single;
+
+Proofterm.proofs := 0;
+
+Context.set_thread_data NONE;
diff -r 31177a9c3025 -r 3c576c7f9731 src/Pure/ROOT
--- a/src/Pure/ROOT	Mon Apr 04 15:35:24 2016 +0200
+++ b/src/Pure/ROOT	Mon Apr 04 15:53:56 2016 +0200
@@ -107,6 +107,7 @@
     "ML/ml_debugger.ML"
     "ML/ml_env.ML"
     "ML/ml_file.ML"
+    "ML/ml_final.ML"
     "ML/ml_heap.ML"
     "ML/ml_lex.ML"
     "ML/ml_name_space.ML"
diff -r 31177a9c3025 -r 3c576c7f9731 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Apr 04 15:35:24 2016 +0200
+++ b/src/Pure/ROOT.ML	Mon Apr 04 15:53:56 2016 +0200
@@ -85,8 +85,6 @@
 use "General/timing.ML";
 use "General/sha1.ML";
 
-val _ = List.app ML_Name_Space.forget_structure ML_Name_Space.critical_structures;
-
 use "PIDE/yxml.ML";
 use "PIDE/document_id.ML";
 
@@ -321,26 +319,11 @@
 
 use "Tools/build.ML";
 use "Tools/named_thms.ML";
-
-structure Output: OUTPUT = Output;  (*seal system channels!*)
-
 use "ML/ml_pp.ML";
-
-
-(* the Pure theory *)
-
 use "ML/ml_file.ML";
 Runtime.toplevel_program (fn () => Thy_Info.use_thy ("Pure", Position.none));
-Context.set_thread_data NONE;
-structure Pure = struct val thy = Thy_Info.pure_theory () end;
 
 
-(* ML toplevel commands *)
+(* final ML setup *)
 
-fun use_thys args =
-  Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
-val use_thy = use_thys o single;
-
-Proofterm.proofs := 0;
-
-structure PolyML = struct structure IntInf = PolyML.IntInf end;
+use "ML/ml_final.ML";