Changes

Summary

1. more operations, notably for profiling;
2. tuned;
3. more compact representation of leaf nodes: only 1.10 .. 1.33 larger than plain list;
4. tuned --- fewer compiler warnings;
5. tuned;
6. tuned;
7. tuned;
8. tuned signature: more uniform structure Key;
9. prefer Sortset.T for shyps;
10. tuned;
11. more operations;
12. tuned names: "e" means "entry" in table.ML and "elem" in set.ML;