# HG changeset patch
# User wenzelm
# Date 1396790362 -7200
# Node ID 7acc933bd7ccc0e0227b7449ddd4a0c5fc3e2b88
# Parent  db69cb14f7eda78b96a302ba855aa25e8bf4fc58
clarified ML bootstrap;

diff -r db69cb14f7ed -r 7acc933bd7cc src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Sun Apr 06 14:30:26 2014 +0200
+++ b/src/Pure/General/secure.ML	Sun Apr 06 15:19:22 2014 +0200
@@ -58,15 +58,3 @@
 
 end;
 
-(*override previous toplevel bindings!*)
-val use_text = Secure.use_text;
-val use_file = Secure.use_file;
-
-fun use s =
-  Position.setmp_thread_data (Position.file_only s)
-    (fn () =>
-      Secure.use_file ML_Parse.global_context true s
-        handle ERROR msg => (writeln msg; error "ML error")) ();
-
-val toplevel_pp = Secure.toplevel_pp;
-
diff -r db69cb14f7ed -r 7acc933bd7cc src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sun Apr 06 14:30:26 2014 +0200
+++ b/src/Pure/ML/ml_context.ML	Sun Apr 06 15:19:22 2014 +0200
@@ -188,7 +188,3 @@
 
 end;
 
-fun use s =
-  ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
-    handle ERROR msg => (writeln msg; error "ML error");
-
diff -r db69cb14f7ed -r 7acc933bd7cc src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Apr 06 14:30:26 2014 +0200
+++ b/src/Pure/ROOT.ML	Sun Apr 06 15:19:22 2014 +0200
@@ -38,6 +38,16 @@
 use "ML/ml_parse.ML";
 use "General/secure.ML";
 
+val use_text = Secure.use_text;
+val use_file = Secure.use_file;
+
+fun use s =
+  Position.setmp_thread_data (Position.file_only s)
+    (fn () =>
+      Secure.use_file ML_Parse.global_context true s
+        handle ERROR msg => (writeln msg; error "ML error")) ();
+
+val toplevel_pp = Secure.toplevel_pp;
 
 
 (** bootstrap phase 1: towards ML within Isar context *)
@@ -236,6 +246,10 @@
 use "ML/ml_context.ML";
 use "ML/ml_antiquotation.ML";
 
+fun use s =
+  ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
+    handle ERROR msg => (writeln msg; error "ML error");
+
 
 
 (** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)