finish updating free_varsTheory