src/Pure/Isar/ROOT.ML

 
 (*derived proof elements*)
 use "local_defs.ML";
 use "calculation.ML";
 use "skip_proof.ML";
+use "obtain.ML";
 
 (*outer syntax*)
 use "comment.ML";
 use "outer_lex.ML";
 use "outer_parse.ML";

   structure Attrib = Attrib;
   structure Method = Method;
   structure LocalDefs = LocalDefs;
   structure Calculation = Calculation;
   structure SkipProof = SkipProof;
+  structure Obtain = Obtain;
   structure Comment = Comment;
   structure OuterLex = OuterLex;
   structure OuterParse = OuterParse;
   structure Toplevel = Toplevel;
   structure Session = Session;