consolidate definitions of `tcbs_of'`

[lsf37]

We have at least two definitions of tcbs_of/tcbs_of' on the master branch, one in the fast path, one in Invariants_H (for at least some architectures).

We should turn these into one.