# HG changeset patch
# User wenzelm
# Date 1243862760 -7200
# Node ID deddd77112b7b08d9ff0a1df29dd915f689e66b4
# Parent  700951b53d2138a44e24edf861fd33cc39354fc4
slightly later setup of ML and secure operations;

diff -r 700951b53d21 -r deddd77112b7 src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Pure/General/ROOT.ML	Mon Jun 01 15:26:00 2009 +0200
@@ -16,10 +16,6 @@
 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";
@@ -34,7 +30,6 @@
 use "path.ML";
 use "url.ML";
 use "buffer.ML";
-use "file.ML";
 use "xml.ML";
 use "yxml.ML";
 
diff -r 700951b53d21 -r deddd77112b7 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Pure/ROOT.ML	Mon Jun 01 15:26:00 2009 +0200
@@ -46,7 +46,15 @@
 use "Syntax/syntax.ML";
 
 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";
 
 (*core of tactical proof system*)
 use "net.ML";