--- a/src/Pure/General/ROOT.ML Wed Jun 22 19:41:23 2005 +0200+++ b/src/Pure/General/ROOT.ML Wed Jun 22 19:41:24 2005 +0200@@ -13,7 +13,6 @@ use "source.ML"; use "symbol.ML"; use "name_space.ML";-use "object.ML"; use "seq.ML"; use "susp.ML"; use "lazy_seq.ML";