Changes

Summary

1. recovered from Unicode accident in 7248d106c607;
2. merged
3. tuned -- fewer warnings;
4. discontinued slightly odd "secure" mode;
5. clarified Pretty.T toplevel pp;
6. clarified modules;
7. clarified modules;
8. tuned header;
9. clarified modules; tuned signature;
10. @{make_string} is available during Pure bootstrap;
11. clarified modules;
12. unused;
13. hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
14. obsolete;
15. tuned signature;
16. obsolete;
17. tuned whitespace;
18. proper ML type;