* ML: Disposed old term read functions (Sign.read_def_terms, Sign.read_term, Thm.read_def_cterms, Thm.read_cterm etc.). INCOMPATIBILITY, should use regular Syntax.read_term, Syntax.read_term_global etc.; see also OldGoals.read_term as last resort for legacy applications.