What you are seeing is sometimes called lexical scoping. The function f was defined in the scope of a certain binding for x, that scope is the only scope that matters in understanding what f does when f is invoked. The fact that x has a different meaning in the scope in which f is invoked doesn't affect the meaning of f itself. In the context of functional programming anything else would violate referential transparency. In the scope of a binding such as

val x = 1

it should be possible to freely replace x by 1. Thus your definition of f should be equivalent to the definition:

def f y = 1 + y

as, indeed, it is.