diff -r c702e2125270 -r f85564116be1 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Sun Jun 25 23:47:12 2000 +0200
+++ b/src/Pure/Isar/ROOT.ML	Sun Jun 25 23:47:47 2000 +0200
@@ -24,19 +24,22 @@
 use "skip_proof.ML";
 
 (*outer syntax*)
+(*use "outer_lex.ML";*)	  (*see ../Thy/ROOT.ML*)
+use "antiquote.ML";
 use "comment.ML";
-(*use "outer_lex.ML";*)	  (*see ../Thy/ROOT.ML*)
 use "outer_parse.ML";
 
 (*toplevel environment*)
 use "toplevel.ML";
 use "session.ML";
+use "isar_output.ML";
 
 (*theory and proof operations*)
 use "isar_thy.ML";
 use "isar_cmd.ML";
 
 (*theory syntax*)
+use "thy_header.ML";
 use "outer_syntax.ML";
 use "isar_syn.ML";
 
@@ -56,13 +59,16 @@
   structure LocalDefs = LocalDefs;
   structure Calculation = Calculation;
   structure SkipProof = SkipProof;
+  structure OuterLex = OuterLex;
+  structure Antiquote = Antiquote;
   structure Comment = Comment;
-  structure OuterLex = OuterLex;
   structure OuterParse = OuterParse;
   structure Toplevel = Toplevel;
   structure Session = Session;
   structure IsarThy = IsarThy;
+  structure IsarOutput = IsarOutput;
   structure IsarCmd = IsarCmd;
+  structure ThyHeader = ThyHeader;
   structure OuterSyntax = OuterSyntax;
   structure IsarSyn = IsarSyn;
   structure Isar = Isar;