# HG changeset patch
# User wenzelm
# Date 936212719 -7200
# Node ID e94cbbe72c5d69f8b786ad735c856dabec62c3d5
# Parent  7e4e286a99314f914862c181cd41cfabd9352718
structure Termtab;

diff -r 7e4e286a9931 -r e94cbbe72c5d 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);