Unplugging Autoinstance. It was responsible for a quadratic behaviour when
defining terms. It was really not used at all, and broken anyway.