src/Pure/ROOT.ML
changeset 4991 d7d525466221
parent 4986 d4f257d3445a
child 5004 cf4e3b487caf
     1.1 --- a/src/Pure/ROOT.ML	Tue Jun 02 15:08:42 1998 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri Jun 05 14:21:11 1998 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4  (*basic utils*)
     1.5  use "library.ML";
     1.6  use "table.ML";
     1.7 +use "object.ML";
     1.8  use "seq.ML";
     1.9  use "name_space.ML";
    1.10  use "term.ML";