src/Pure/ROOT.ML
changeset 5017 786a17461ab9
parent 5004 cf4e3b487caf
child 5092 e443bc494604
--- a/src/Pure/ROOT.ML	Wed Jun 10 11:54:04 1998 +0200
+++ b/src/Pure/ROOT.ML	Wed Jun 10 11:55:09 1998 +0200
@@ -13,12 +13,9 @@
 ml_prompts "> " "# ";
 
 
-(*basic utils*)
+(*basic tools*)
 use "library.ML";
-use "table.ML";
-use "object.ML";
-use "seq.ML";
-use "name_space.ML";
+cd "General"; use "ROOT.ML"; cd "..";
 use "term.ML";
 
 (*inner syntax module*)