forbid extending sort K in the Java backend

Fixed https://github.com/kframework/k/issues/708

@dwightguth @radumereuta please review
Not sure about this, we probably want substitution to be a function and return a K.  Or even have one for KItem and one for K.  Traian?