diff -r 2ea20e5fdf16 -r 3b0d7a417a8b NEWS
--- a/NEWS	Thu Jun 19 22:05:05 2008 +0200
+++ b/NEWS	Thu Jun 19 22:27:10 2008 +0200
@@ -61,9 +61,10 @@
 the variables are specified as plain indexnames, not string encodings
 thereof.  INCOMPATIBILITY.
 
-* 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,
+* Disposed old type and term read functions (Sign.read_def_typ,
+Sign.read_typ, Sign.read_def_terms, Sign.read_term,
+Thm.read_def_cterms, Thm.read_cterm etc.).  INCOMPATIBILITY, should
+use regular Syntax.read_typ, Syntax.read_term, Syntax.read_typ_global,
 Syntax.read_term_global etc.; see also OldGoals.read_term as last
 resort for legacy applications.