I don't know what makes you claim that the current semantics of priorities is 'wrong'.
We chose to implement priorities this way because it is a simple system that is easy to explain and easy to implement. The fact that it doesn't handle your example doesn't convince me. It's not something that is widely used in programming languages. It could be potentially be handled by the full general rewrite engine.
Even so. Now it's not the time to 'fix' this. First of all, we need a replacement for SDF, and after that we can think of ways to extend it.

Regarding the concrete syntax trees... I don't know where you got this from. All the parsing systems that I've worked with produce abstract syntax trees. And for good reasons, it makes everything more complicated. The current infrastructure of K has problems handling this format. The latex and html backends need to be modified. Also if you want the split that Grigore wants between front-end and backend, you will need two versions of latex and html...
I think the better solution here is to solve the problems with labels referencing multiple productions. That's what TermCons does (in a weird way). I think the best solution for this case would be to have two levels of klabels:
1. for parsing - maybe derived from the `cons` field? At this level I will solve all the ambiguities (priorities, associativity...)
2. for the rest of the compilation steps.

You mentioned the parser returning TermCons. That's kind of hard to do. The parser actually creates `KList`s, and WrapLabelRule only puts a KApp with a label on top of that. TermCons has the list of children builtin. It would require heavy modifications either for the parser, or for everything that uses TermCons.

KApp is more flexible. This is also why I added it to the filters. I want to remove TermCons at the same time with the SDF parser.

I hope I'm making sense.