Fix some mistakes in datatypes theory combination, disable two regressions.  Minor fix for fun defs.