--- a/src/Pure/term.ML Thu Feb 05 11:20:35 1998 +0100
+++ b/src/Pure/term.ML Fri Feb 06 11:18:29 1998 +0100
@@ -1007,3 +1007,4 @@
structure BasicTerm: BASIC_TERM = Term;
open BasicTerm;
+structure Vartab = TableFun(type key = indexname val ord = Term.indexname_ord);