--- a/src/Pure/Isar/ROOT.ML Fri Nov 03 18:33:57 2000 +0100
+++ b/src/Pure/Isar/ROOT.ML Fri Nov 03 21:25:10 2000 +0100
@@ -71,5 +71,6 @@
structure ThyHeader = ThyHeader;
structure OuterSyntax = OuterSyntax;
structure IsarSyn = IsarSyn;
+ structure Obtain = Obtain;
structure Isar = Isar;
end;