clarified signature;

clarified signature: prefer proper order operation;

sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
minor tuning;

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;
tuned some error messages;

modernized structure Term_Ord;

further standard instances of functor Graph;

just one copy of structure Term_Graph (in Pure);

added term_cache;
tuned;

Sorttab in Pure;

renamed functor TableFun to Table, and GraphFun to Graph;

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;