Now loads symtab.ML before term.ML. Functor
authorpaulson
Fri Dec 22 10:11:35 1995 +0100 (1995-12-22)
changeset 1411f60f68878354
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
     1.1 --- a/src/Pure/ROOT.ML	Wed Dec 20 16:28:51 1995 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Fri Dec 22 10:11:35 1995 +0100
     1.3 @@ -17,10 +17,8 @@
     1.4  print_depth 1;
     1.5  
     1.6  use "library.ML";
     1.7 +use "symtab.ML";
     1.8  use "term.ML";
     1.9 -use "symtab.ML";
    1.10 -
    1.11 -structure Symtab = SymtabFun();
    1.12  
    1.13  (*Syntax module*)
    1.14  cd "Syntax";
    1.15 @@ -68,7 +66,6 @@
    1.16  structure CPure = struct val thy = cpure_thy end;
    1.17  
    1.18  (* hide functors; saves space in PolyML *)
    1.19 -functor SymtabFun() = struct end;
    1.20  functor TypeFun() = struct end;
    1.21  functor SignFun() = struct end;
    1.22  functor SequenceFun() = struct end;