tweak to fix proof in hol_kernelScript.sml
make hol_kernel track new_const and new_type

and slightly rework the STATE invariant