src/Pure/term.ML
changeset 4604 ff8eca799c8f
parent 4493 26511042ce07
child 4626 51dd12f34c78
--- 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);