src/Pure/Isar/ROOT.ML

--- a/src/Pure/Isar/ROOT.ML	Thu Apr 22 11:00:03 2004 +0200
+++ b/src/Pure/Isar/ROOT.ML	Thu Apr 22 11:00:22 2004 +0200
@@ -43,6 +43,7 @@
 
 (*theory and proof operations*)
 use "isar_thy.ML";
+use "constdefs.ML";
 use "isar_cmd.ML";
 use "isar_syn.ML";
 
@@ -73,6 +74,7 @@
   structure ThyHeader = ThyHeader;
   structure OuterSyntax = OuterSyntax;
   structure IsarThy = IsarThy;
+  structure Constdefs = Constdefs;
   structure IsarCmd = IsarCmd;
   structure IsarSyn = IsarSyn;
   structure Isar = Isar;