# HG changeset patch
# User wenzelm
# Date 932156522 -7200
# Node ID 0073aa5715026cd13e1d160528a8c17d2a4cd47b
# Parent  75ff179df7b761f7668ee4e150d5ba1bb0fce41b
structure LocalDefs = LocalDefs;
structure Calculation = Calculation;
structure SkipProof = SkipProof;

diff -r 75ff179df7b7 -r 0073aa571502 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Fri Jul 16 14:06:13 1999 +0200
+++ b/src/Pure/Isar/ROOT.ML	Fri Jul 16 22:22:02 1999 +0200
@@ -49,6 +49,9 @@
   structure Args = Args;
   structure Attrib = Attrib;
   structure Method = Method;
+  structure LocalDefs = LocalDefs;
+  structure Calculation = Calculation;
+  structure SkipProof = SkipProof;
   structure Comment = Comment;
   structure OuterLex = OuterLex;
   structure OuterParse = OuterParse;