src/Pure/ROOT.ML
changeset 3763 31ec17820f49
parent 3508 089806e6133b
child 3864 e0ce3d4ec47d
--- a/src/Pure/ROOT.ML	Wed Oct 01 17:32:38 1997 +0200
+++ b/src/Pure/ROOT.ML	Wed Oct 01 17:36:51 1997 +0200
@@ -18,6 +18,7 @@
 
 use "library.ML";
 use "symtab.ML";
+use "name_space.ML";
 use "term.ML";
 
 (*Syntax module*)