src/Pure/ROOT.ML

 val version = "Isabelle-94 revision 4: August 95";
 
 print_depth 1;
 
 use "library.ML";
+use "symtab.ML";
 use "term.ML";
-use "symtab.ML";
-
-structure Symtab = SymtabFun();
 
 (*Syntax module*)
 cd "Syntax";
 use "ROOT.ML";
 cd "..";

 
 structure Pure = struct val thy = pure_thy end;
 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;
 functor EnvirFun() = struct end;
 functor PatternFun() = struct end;