[small refactoring] Generalization.ml: split the 'exit' function in simpler parts.

This small refactoring is part of the work we did with @omartino on frozen constraints. ("collaprog" is the name of the machine on which we do pair-programming-through-SSH.) It makes the code of Generalization.exit more readable, and also easier to change:

• The "level adjustment" logic does not fundamentally need to be part of the exit function, as it could in theory be called several times on the young generation. Taking it out as a separate function reflects this different role (compared to other part of generalization that really are destructive operations.)
• In our own changes (not included here) for frozen constraints, we need to run code after levels have been adjusted, but before generalization itself takes place. The refactoring makes this easier.