Remove unnecessary code given change to s-expressions as theory data

The implementation of DiskThms is now dramatically simpler.

Make non-kernel code that depends on SharingTables work again

I think it's clear that the SharingTables stuff should build towards a
standardised input/output format that is easy to embed into other
formats. I think perhaps s-expressions are the way to go here.

Fix p/printers and selftests to agree with one another again

Change src/bool to src/1 as a prelude to experimentation!