src/Pure/General/ROOT.ML
changeset 14831 7c37c18a6188
parent 14594 3ff9cfc5c403
child 16136 1cb99d74eebb
--- a/src/Pure/General/ROOT.ML	Sat May 29 15:05:25 2004 +0200
+++ b/src/Pure/General/ROOT.ML	Sat May 29 15:05:37 2004 +0200
@@ -5,6 +5,7 @@
 *)
 
 use "table.ML";
+use "output.ML";
 use "scan.ML";
 use "source.ML";
 use "symbol.ML";
@@ -22,12 +23,12 @@
 use "file.ML";
 use "buffer.ML";
 use "history.ML";
-use "pretty.ML";
 use "xml.ML";
 
 structure PureGeneral =
 struct
   structure Symtab = Symtab;
+  structure Output = Output;
   structure Graph = Graph;
   structure Object = Object;
   structure Seq = Seq;
@@ -41,6 +42,5 @@
   structure File = File;
   structure Buffer = Buffer;
   structure History = History;
-  structure Pretty = Pretty;
   structure XML = XML;
 end;