* 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.

Reply via email to