structure Obtain = Obtain;
authorwenzelm
Fri, 03 Nov 2000 21:25:10 +0100
changeset 10376 e265443c210f
parent 10375 d943898cc3a9
child 10377 6b595f9ae37e
structure Obtain = Obtain;
src/Pure/Isar/ROOT.ML
--- 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;