src/Pure/ROOT.ML
changeset 31326 deddd77112b7
parent 30834 1640e0625301
child 31333 fcd010617e6c
     1.1 --- a/src/Pure/ROOT.ML	Mon Jun 01 15:26:00 2009 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon Jun 01 15:26:00 2009 +0200
     1.3 @@ -46,7 +46,15 @@
     1.4  use "Syntax/syntax.ML";
     1.5  
     1.6  use "type_infer.ML";
     1.7 +
     1.8 +(*ML support*)
     1.9 +use "ML/ml_lex.ML";
    1.10 +use "ML/ml_parse.ML";
    1.11  use "ML/ml_syntax.ML";
    1.12 +use "ML/ml_env.ML";
    1.13 +
    1.14 +use "General/secure.ML";
    1.15 +use "General/file.ML";
    1.16  
    1.17  (*core of tactical proof system*)
    1.18  use "net.ML";