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.

Also postpend "_conj" to all conjectures/axioms for easy recognition in output of tptp exporter.