Change theory files to use an s-expression representation

This wastes some disk-space in the form of extra white-space that the
Oppen pretty-printer introduces for indentation purposes, but with the
string table used, the number of lines and the number of
non-whitespace characters is lower.

The string table can and will be used in more places in subsequent
commits to try to improve file size and sharing. The theory data may
also shift to directly use s-expressions rather than strings (people
wedded to a string representation can always embed those into
s-expressions of course).

Complete basic Poly implementation of TheoryIO (separate dat files)

Still to tweak Holmake and to make sure it all works on Moscow ML

Use _Theory.dat for loading theory data into _Theory.sml