diff -r ff827fccffb5 -r 123b215882ae src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Wed May 12 17:58:03 1999 +0200
+++ b/src/Pure/Isar/ROOT.ML	Sat May 15 16:15:54 1999 +0200
@@ -38,16 +38,18 @@
 struct
   structure ProofContext = ProofContext;
   structure Proof = Proof;
+  structure ProofHistory = ProofHistory;
   structure Args = Args;
   structure Attrib = Attrib;
   structure Method = Method;
+  structure Comment = Comment;
   structure OuterLex = OuterLex;
   structure OuterParse = OuterParse;
-  structure ProofHistory = ProofHistory;
   structure Toplevel = Toplevel;
-  structure OuterSyntax = OuterSyntax;
+  structure Session = Session;
   structure IsarThy = IsarThy;
   structure IsarCmd = IsarCmd;
+  structure OuterSyntax = OuterSyntax;
   structure IsarSyn = IsarSyn;
   structure Isar = Isar;
 end;