structure Termtab;
authorwenzelm
Wed, 01 Sep 1999 21:05:19 +0200
changeset 7406 e94cbbe72c5d
parent 7405 7e4e286a9931
child 7407 fc8cad55af74
structure Termtab;
src/Pure/term.ML
--- 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);