changeset 31976 | 17414e2736f4 |
parent 31971 | 8c1b845ed105 |
child 32841 | 57dcddf81b01 |
--- a/src/Pure/term_ord.ML Thu Jul 09 22:13:19 2009 +0200 +++ b/src/Pure/term_ord.ML Thu Jul 09 22:36:11 2009 +0200 @@ -205,5 +205,6 @@ end; structure Vartab = Table(type key = indexname val ord = TermOrd.fast_indexname_ord); +structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord); structure Typtab = Table(type key = typ val ord = TermOrd.typ_ord); structure Termtab = Table(type key = term val ord = TermOrd.fast_term_ord);