Hello,
I recently got bad performance out of TLC for no apparent reason. Then I found out that my specification contained a definition of the form Def == Expr, where Expr was expensive to evaluate. Def was not used at all in the rest of my specification, however it seemed that TLC evaluated it anyway. After commenting it out, the performance of TLC was back to what I would expect.
So one should comment out unneeded definitions to prevent TLC from evaluating them.
Giuliano