--- 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;