Now loads symtab.ML before term.ML. Functor
authorpaulson
Fri, 22 Dec 1995 10:11:35 +0100
changeset 1411 f60f68878354
parent 1410 324aa8134639
child 1412 2ab32768c996
Now loads symtab.ML before term.ML. Functor > SymtabFun has been changed to the structure Symtab.
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;