Merge 'not unified' variables

That is, explicitly given variables which could otherwise be unified. If
they appear several times in the notunified list, make sure they all
match.

Fixes #1077