Refactored label comparison

[samsa1]

Factored together the code to compare labels during unification.

This is just reducing code duplication and does not have any impact on the user. I think this might not require a Changes entry.

This refactor was motivated by modular explicit that might require more label comparison.

[gasche]

This looks fine but I don't think that in_pattern_mode should be an optional parameter: if you forget to use it when you should, the compiler is unsound (in a very very small corner case). Let's make it mandatory.