# HG changeset patch
# User wenzelm
# Date 1085835937 -7200
# Node ID 7c37c18a618825c91e032669df3014ed0e116ba2
# Parent  faa4865ba1ce28e9d268ca90d076c824135c9032
added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;

diff -r faa4865ba1ce -r 7c37c18a6188 src/Pure/General/ROOT.ML
--- 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;