# HG changeset patch
# User wenzelm
# Date 1119462084 -7200
# Node ID 7318c205a67f11c069348d284ef9739a5a73d2aa
# Parent  954495db0f0719ca1a8f2f9a39c4fa57d9904844
removed obsolete object.ML (see Pure/library.ML);

diff -r 954495db0f07 -r 7318c205a67f src/Pure/General/ROOT.ML
--- 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";