diff -r 324aa8134639 -r f60f68878354 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Dec 20 16:28:51 1995 +0100
+++ b/src/Pure/ROOT.ML	Fri Dec 22 10:11:35 1995 +0100
@@ -17,10 +17,8 @@
 print_depth 1;
 
 use "library.ML";
+use "symtab.ML";
 use "term.ML";
-use "symtab.ML";
-
-structure Symtab = SymtabFun();
 
 (*Syntax module*)
 cd "Syntax";
@@ -68,7 +66,6 @@
 structure CPure = struct val thy = cpure_thy end;
 
 (* hide functors; saves space in PolyML *)
-functor SymtabFun() = struct end;
 functor TypeFun() = struct end;
 functor SignFun() = struct end;
 functor SequenceFun() = struct end;