Now loads symtab.ML before term.ML. Functor
> SymtabFun has been changed to the structure Symtab.
--- 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;