diff -r df19e1de5c8a -r f4fe91b3b6db src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Mon Nov 16 10:44:30 1998 +0100
+++ b/src/Pure/Isar/ROOT.ML	Mon Nov 16 10:44:55 1998 +0100
@@ -26,3 +26,21 @@
 use "isar_thy.ML";
 use "isar_cmd.ML";
 use "isar_syn.ML";
+
+
+structure PureIsar =
+struct
+  structure ProofContext = ProofContext;
+  structure Proof = Proof;
+  structure Args = Args;
+  structure Attrib = Attrib;
+  structure Method = Method;
+  structure OuterLex = OuterLex;
+  structure OuterParse = OuterParse;
+  structure ProofHistory = ProofHistory;
+  structure Toplevel = Toplevel;
+  structure OuterSyntax = OuterSyntax;
+  structure IsarThy = IsarThy;
+  structure IsarCmd = IsarCmd;
+  structure IsarSyn = IsarSyn;
+end;