# HG changeset patch
# User wenzelm
# Date 1243941316 -7200
# Node ID ba5b7749fa61f45457160823c3a37c742981f506
# Parent  999fa9e1dbdde066737267adf9ee10da420f7cf4
early setup of secure operations (again, cf. deddd77112b7) -- NB: fix_ints is required for bootstrap;
late setup of ML_Env and ML_Compiler;

diff -r 999fa9e1dbdd -r ba5b7749fa61 src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Mon Jun 01 23:28:07 2009 +0200
+++ b/src/Pure/General/ROOT.ML	Tue Jun 02 13:15:16 2009 +0200
@@ -16,6 +16,10 @@
 use "position.ML";
 use "symbol_pos.ML";
 use "antiquote.ML";
+use "../ML/ml_lex.ML";
+use "../ML/ml_parse.ML";
+use "secure.ML";
+
 use "integer.ML";
 use "stack.ML";
 use "queue.ML";
@@ -30,6 +34,7 @@
 use "path.ML";
 use "url.ML";
 use "buffer.ML";
+use "file.ML";
 use "xml.ML";
 use "yxml.ML";
 
diff -r 999fa9e1dbdd -r ba5b7749fa61 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Mon Jun 01 23:28:07 2009 +0200
+++ b/src/Pure/Isar/ROOT.ML	Tue Jun 02 13:15:16 2009 +0200
@@ -24,6 +24,13 @@
 use "outer_parse.ML";
 use "value_parse.ML";
 use "args.ML";
+
+(*ML support*)
+use "../ML/ml_syntax.ML";
+use "../ML/ml_env.ML";
+if ml_system = "polyml-experimental"
+then use "../ML/ml_compiler_polyml-5.3.ML"
+else use "../ML/ml_compiler.ML";
 use "../ML/ml_context.ML";
 
 (*theory sources*)
diff -r 999fa9e1dbdd -r ba5b7749fa61 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Jun 01 23:28:07 2009 +0200
+++ b/src/Pure/ROOT.ML	Tue Jun 02 13:15:16 2009 +0200
@@ -47,19 +47,6 @@
 
 use "type_infer.ML";
 
-(*ML support*)
-use "ML/ml_lex.ML";
-use "ML/ml_parse.ML";
-use "ML/ml_syntax.ML";
-use "ML/ml_env.ML";
-
-use "General/secure.ML";
-use "General/file.ML";
-
-if ml_system = "polyml-experimental"
-then use "ML/ml_compiler_polyml-5.3.ML"
-else use "ML/ml_compiler.ML";
-
 (*core of tactical proof system*)
 use "net.ML";
 use "item_net.ML";