slightly later setup of ML and secure operations;
authorwenzelm
Mon Jun 01 15:26:00 2009 +0200 (2009-06-01)
changeset 31326deddd77112b7
parent 31325 700951b53d21
child 31327 ffa5356cc343
slightly later setup of ML and secure operations;
src/Pure/General/ROOT.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/General/ROOT.ML	Mon Jun 01 15:26:00 2009 +0200
     1.2 +++ b/src/Pure/General/ROOT.ML	Mon Jun 01 15:26:00 2009 +0200
     1.3 @@ -16,10 +16,6 @@
     1.4  use "position.ML";
     1.5  use "symbol_pos.ML";
     1.6  use "antiquote.ML";
     1.7 -use "../ML/ml_lex.ML";
     1.8 -use "../ML/ml_parse.ML";
     1.9 -use "secure.ML";
    1.10 -
    1.11  use "integer.ML";
    1.12  use "stack.ML";
    1.13  use "queue.ML";
    1.14 @@ -34,7 +30,6 @@
    1.15  use "path.ML";
    1.16  use "url.ML";
    1.17  use "buffer.ML";
    1.18 -use "file.ML";
    1.19  use "xml.ML";
    1.20  use "yxml.ML";
    1.21  
     2.1 --- a/src/Pure/ROOT.ML	Mon Jun 01 15:26:00 2009 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Mon Jun 01 15:26:00 2009 +0200
     2.3 @@ -46,7 +46,15 @@
     2.4  use "Syntax/syntax.ML";
     2.5  
     2.6  use "type_infer.ML";
     2.7 +
     2.8 +(*ML support*)
     2.9 +use "ML/ml_lex.ML";
    2.10 +use "ML/ml_parse.ML";
    2.11  use "ML/ml_syntax.ML";
    2.12 +use "ML/ml_env.ML";
    2.13 +
    2.14 +use "General/secure.ML";
    2.15 +use "General/file.ML";
    2.16  
    2.17  (*core of tactical proof system*)
    2.18  use "net.ML";