src/Pure/Isar/ROOT.ML
changeset 7680 27bbbe36d49a
parent 7021 0073aa571502
child 7728 2e737ce3cdb5
--- a/src/Pure/Isar/ROOT.ML	Fri Oct 01 20:39:40 1999 +0200
+++ b/src/Pure/Isar/ROOT.ML	Fri Oct 01 20:40:03 1999 +0200
@@ -19,6 +19,7 @@
 use "local_defs.ML";
 use "calculation.ML";
 use "skip_proof.ML";
+use "obtain.ML";
 
 (*outer syntax*)
 use "comment.ML";
@@ -52,6 +53,7 @@
   structure LocalDefs = LocalDefs;
   structure Calculation = Calculation;
   structure SkipProof = SkipProof;
+  structure Obtain = Obtain;
   structure Comment = Comment;
   structure OuterLex = OuterLex;
   structure OuterParse = OuterParse;