diff -r 67c5966611c6 -r 786a17461ab9 src/Pure/ROOT.ML
--- 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*)