src/Pure/term_ord.ML
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);