src/Pure/term_subst.ML
2006-11-30 ago zero_var_indexes_inst: multiple terms;
2006-11-12 ago instantiate: tuned indentity case;
2006-11-05 ago instantiate: avoid global references;
2006-09-12 ago Efficient term substitution -- avoids copying.