Yes, of course; I meant primed.
After some experimentation, I now understand my problem better. Suppose I have these declarations:
VARIABLES x, y
Foo(a) == a \cup y
If I then use the primed formula Foo(x)', it will prime both x and y, but in my situation only y' is already determined in the evaluation, so TLC will emit the usual error in such cases, "The identifier x is either undefined or not an operator".
Trying to get around this seems to be of no use:
LET t == x IN Foo(t)'
yields the same result. Other transformations don't change the situation:
LET t == x[5].a \cap {2, 3} IN Foo(t)'
Is there a way to capture a value from a variable and pass it into a formula in such a way that priming it will not try to lazily obtain the value from the variable (or, simply put, "forget" the value's dependence on the variable)? While I see the merits of such evaluation, it can also be quite confusing (as in my case), because the value passed to the function is a result of several non-trivial transformations, that it's easy to miss the value's dependence on a variable.
Ron