The payload of this change is to ensure that a bottoming function
still has an unfolding, just one with an UnfoldingGuidance of
UnfoldNever.

Previously it was getting an unfolding of NoUnfolding. I don't think
that was really /wrong/, but it was inconsistent with the general
principle of giving everthing an unfoding if we know it.  And it
seems tideier this way.