Thanks for this. But I'm not talking about the Kleisli Category $C_T$, I am talking about the Kleisli triple over $C$ (sorry, this was my mistake; I'll edit the question). In every place where I have seen the Kleisli triple defined from a Monad, the underlying Category is the same with no indexing of objects. When you index the objects, surely it is a different category, however you present the theory.

I thought that * has to be defined on the whole class of morphisms. Even if you restricted it to Hom(A,TB), the initial problem is still there because I might define it differently on Hom(A,TC) but TB=TC. Could you give a precise mathematical definition that makes sense (forget Isabelle for the moment)?

I was thinking about this, but that's a different category, isn't it?

Maybe I did not make myself clear enough. It is a subtle point (maybe trivial?), and one that I missed until I tried to formally write down a definition in Isabelle. Given a monad $(T,\mu,\eta)$, I need to define $*$ on the class $\{f|\exists A,B \in |\mathbf{C}| . f : A \to T B \}$. If $T$ were an embedding then I could just take $B := T^{-1}(\mathrm{cod}(f))$. What do I do though when $T$ is not an embedding? All I know about the codomain of an element of this class is that it is in the image of $T$. There may be many $B$'s and the $\mu_B$'s may be different!