1) remove trm_of_thm,  thm is represented as term in the format of (term list, term)
2) some renaming