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