The translation of definitions still fails when the type of definiens cannot be inferred (correctly) in that case no definition is generated

Since the HOL Peano numbers theory includes simple function types with cause notation clashes with dependent function types.