src/Pure/ROOT.ML
changeset 5017 786a17461ab9
parent 5004 cf4e3b487caf
child 5092 e443bc494604
     1.1 --- a/src/Pure/ROOT.ML	Wed Jun 10 11:54:04 1998 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed Jun 10 11:55:09 1998 +0200
     1.3 @@ -13,12 +13,9 @@
     1.4  ml_prompts "> " "# ";
     1.5  
     1.6  
     1.7 -(*basic utils*)
     1.8 +(*basic tools*)
     1.9  use "library.ML";
    1.10 -use "table.ML";
    1.11 -use "object.ML";
    1.12 -use "seq.ML";
    1.13 -use "name_space.ML";
    1.14 +cd "General"; use "ROOT.ML"; cd "..";
    1.15  use "term.ML";
    1.16  
    1.17  (*inner syntax module*)