forbid extending sort K in the Java backend

Fixed https://github.com/kframework/k/issues/708

@dwightguth @radumereuta please review
Yes, of course. But my change is to mechanically replace ```syntax K ::=``` with ```syntax KItem ::=``` for non-function productions. This improvement should be done in another commit by whoever owns this file.