src/Pure/ROOT.ML
changeset 1411 f60f68878354
parent 1228 7d6b0241afab
child 1443 ff8a804e0201
     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;