src/Pure/term_ord.ML
2011-07-13 ago sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
2010-07-20 ago eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
2010-02-27 ago modernized structure Term_Ord;
2010-02-27 ago further standard instances of functor Graph;
2010-02-27 ago just one copy of structure Term_Graph (in Pure);
2009-10-01 ago added term_cache;
2009-07-09 ago Sorttab in Pure;
2009-07-09 ago renamed functor TableFun to Table, and GraphFun to Graph;
2008-12-31 ago moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);