diff -r c66545fe72bf -r 1cb99d74eebb src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Tue May 31 11:53:26 2005 +0200
+++ b/src/Pure/General/ROOT.ML	Tue May 31 11:53:27 2005 +0200
@@ -6,17 +6,17 @@
 
 use "table.ML";
 use "output.ML";
+use "graph.ML";
+use "heap.ML";
 use "scan.ML";
 use "source.ML";
 use "symbol.ML";
-use "graph.ML";
-use "heap.ML";
+use "name_space.ML";
 use "object.ML";
 use "seq.ML";
 use "susp.ML";
 use "lazy_seq.ML";
 use "lazy_scan.ML";
-use "name_space.ML";
 use "position.ML";
 use "path.ML";
 use "url.ML";
@@ -24,23 +24,3 @@
 use "buffer.ML";
 use "history.ML";
 use "xml.ML";
-
-structure PureGeneral =
-struct
-  structure Symtab = Symtab;
-  structure Output = Output;
-  structure Graph = Graph;
-  structure Object = Object;
-  structure Seq = Seq;
-  structure NameSpace = NameSpace;
-  structure Position = Position;
-  structure Scan = Scan;
-  structure Source = Source;
-  structure Symbol = Symbol;
-  structure Path = Path;
-  structure Url = Url;
-  structure File = File;
-  structure Buffer = Buffer;
-  structure History = History;
-  structure XML = XML;
-end;