src/Pure/compress.ML
2007-07-29 ago NAMED_CRITICAL;
2007-07-23 ago marked some CRITICAL sections (for multithreading);
2007-05-07 ago simplified DataFun interfaces;
2006-09-15 ago renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-01 ago curried_lookup/update;
2005-08-01 ago compression of terms and types by sharing common subtrees;