tuned;
clarified type Indexname, with plain value Int; eliminated pointless cache_int;
tuned header;
tuned output;
more general cache, also for term substructures;