src/Pure/term_ord.ML
changeset 31971 8c1b845ed105
parent 29269 5c25a2012975
child 31976 17414e2736f4
     1.1 --- a/src/Pure/term_ord.ML	Thu Jul 09 17:34:59 2009 +0200
     1.2 +++ b/src/Pure/term_ord.ML	Thu Jul 09 22:01:41 2009 +0200
     1.3 @@ -204,6 +204,6 @@
     1.4  
     1.5  end;
     1.6  
     1.7 -structure Vartab = TableFun(type key = indexname val ord = TermOrd.fast_indexname_ord);
     1.8 -structure Typtab = TableFun(type key = typ val ord = TermOrd.typ_ord);
     1.9 -structure Termtab = TableFun(type key = term val ord = TermOrd.fast_term_ord);
    1.10 +structure Vartab = Table(type key = indexname val ord = TermOrd.fast_indexname_ord);
    1.11 +structure Typtab = Table(type key = typ val ord = TermOrd.typ_ord);
    1.12 +structure Termtab = Table(type key = term val ord = TermOrd.fast_term_ord);