removed obsolete object.ML (see Pure/library.ML);
authorwenzelm
Wed Jun 22 19:41:24 2005 +0200 (2005-06-22)
changeset 165387318c205a67f
parent 16537 954495db0f07
child 16539 60adb8b28377
removed obsolete object.ML (see Pure/library.ML);
src/Pure/General/ROOT.ML
     1.1 --- a/src/Pure/General/ROOT.ML	Wed Jun 22 19:41:23 2005 +0200
     1.2 +++ b/src/Pure/General/ROOT.ML	Wed Jun 22 19:41:24 2005 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4  use "source.ML";
     1.5  use "symbol.ML";
     1.6  use "name_space.ML";
     1.7 -use "object.ML";
     1.8  use "seq.ML";
     1.9  use "susp.ML";
    1.10  use "lazy_seq.ML";