Factor out HOL kernel.
Add dest-theorem

Also: fix whitespace and sterner warnings.
Add MK-COMB

Also following HOL-Light in crazy capitalisation. I nearly made mk-comb recursive.
Fix tests.

Need to make a note: using nil for failure means that error messages are difficult to track down. Could go for more defence. In this case, we were trying to create an equation between terms not in the :hol context. This caused a nil type to appear somewhere which gets reported as a context failure.
Factor hol into main kernel. Put thin abstractions over all terms and types.
Add asserts to catch "type" errors.