src/Pure/General/ROOT.ML

--- a/src/Pure/General/ROOT.ML	Wed May 12 17:58:03 1999 +0200
+++ b/src/Pure/General/ROOT.ML	Sat May 15 16:15:54 1999 +0200
@@ -29,12 +29,12 @@
   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 Source = Source;
   structure Pretty = Pretty;
 end;