src/Pure/General/ROOT.ML
changeset 6180 99f107fd478f
parent 6136 166b3353aad5
child 6222 2b24cf477313
--- a/src/Pure/General/ROOT.ML	Wed Feb 03 16:28:13 1999 +0100
+++ b/src/Pure/General/ROOT.ML	Wed Feb 03 16:28:38 1999 +0100
@@ -17,6 +17,7 @@
 use "source.ML";
 use "symbol.ML";
 use "pretty.ML";
+use "use.ML";
 
 structure PureGeneral =
 struct
@@ -33,4 +34,5 @@
   structure Source = Source;
   structure Symbol = Symbol;
   structure Pretty = Pretty;
+  structure Use = Use;
 end;