Tidy up modularisation in Hol_pp and DB.

[mn200]

In particular:

• the THEORY data type should probably be in Theory.sig
• there's no obvious reason why DB gets print_theory and Hol_pp doesn't. On the other hand, it's not obvious why Hol_pp exists at all as it is basically just a filtered version of entry-points from Parse

---

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.