| changeset 7406 | e94cbbe72c5d |
| parent 7318 | 768fab6dae74 |
| child 7638 | f586d7995474 |
--- a/src/Pure/term.ML Wed Sep 01 21:04:59 1999 +0200 +++ b/src/Pure/term.ML Wed Sep 01 21:05:19 1999 +0200 @@ -1041,4 +1041,6 @@ structure BasicTerm: BASIC_TERM = Term; open BasicTerm; + structure Vartab = TableFun(type key = indexname val ord = Term.indexname_ord); +structure Termtab = TableFun(type key = term val ord = Term.term_ord);