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;