> That was my original intuition. I don't know what TLA+'s policy on backwards compatibility is, but changing the action semantics of CHOOSE now may break existing specs in possibly subtle ways.
No, it shouldn't. A CHOOSE _expression_ returns a value, i.e., a constant. So the proposed change doesn't break the semantics but only the level-checking algorithm, which we know to be an approximation.
Capture(e) == CHOOSE k \in {e} : k = e
Next == /\ x' = x + 1
/\ PrintT(x) \* => 1
/\ PrintT(x') \* => 2
/\ PrintT(Capture(x)) \* => 1
/\ PrintT(Capture(x)') \* => 2
Spec == (x = 1) /\ [][Next]_<<x>>
So Capture(x)' /= Capture(x), and this seems to be more than just level-checking.
If the difference is due to my writing `CHOOSE k \in {e} : k = e` instead of `CHOOSE k : k = e`, then the latter is currently unsupported by TLC anyway.