# HG changeset patch # User paulson # Date 819623495 -3600 # Node ID f60f68878354e3585445ada779d110927af45a3d # Parent 324aa813463903614341644e0bbc8213dd5f8e2c Now loads symtab.ML before term.ML. Functor > SymtabFun has been changed to the structure Symtab. 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;