use new computeLib.add_datatype_info
update compile_primitivesTheory for recent additions to HOL