Improve TypeBase API for reporting on record fields

Datatype code now bypasses treatment of "big records". This stuff can
all be deleted and I will be happy to see it go as it is horrifically
complicated, and usually only serves to confuse users.

Thanks to a CakeML Slack discussion for the push to make the API
change.

Fix bug in handling of distinctness for large enumerated types

Previous attempt at regression test for this didn't capture scenario
where srw_ss() had already been initialised and correctness relied on
TypeBase hook telling BasicProvers about newly arriving tyinfo.

Performance is still bad when theories dump large tyinfos to disk.

Re-implement Datatype package with TypeBase sexps (not adjoin)