The Toolbox generates an MC.tla file upon TLC startup which extends the

actual specification being verified. Additionally, to evaluate any
constant expression, MC.tla also extends TLC.tla to use the PrintT
operator defined in TLC.tla  (and its module override tlc2.module.TLC):
"ASSUME PrintT(...)"

Extending TLC.tla in MC.tla can cause a name clash if the actual
specification does *not* extend TLC and happens to declare an operator
colliding with one in TLC.tla (e.g. "Permutations", "SortSeq", ...).

To resolve this name clash, the Toolbox no longer extends TLC.tla in
MC.tla but instead generates a LOCAL declaration of PrintT:
"LOCAL PrintT(out) == TRUE
 ASSUME PrintT(...)"

TLC.tla's PrintT is override by the tlc2.module.TLC#PrintT module
override. Thus, the LOCAL construct above only resolves the name clash
at the SANY level, but produces no output. This class effectively
associates MC.tla's PrintT with tlc2.module.TLC#PrintT.

The only operator for which this approach obviously does not work is
PrintT itself. If the actual specification declares PrintT, evaluating a
constant expression will fail. However - contrary to
Permutations/SortSeq/... - this is handled gracefully with a proper
error message.

Fixes Github issue #103
https://github.com/tlaplus/tlaplus/issues/103

[Bug][Toolbox]