Bug 593 fix: if the type is finite, it is now considered for detecting theories of nested terms.