# HG changeset patch
# User wenzelm
# Date 1213823741 -7200
# Node ID 1e9c05cddc64b6f14909352bc80d30a07e9c3d2f
# Parent  1d8c6703c7b11a8a8d72b8943f76f6730dd20da4
* Disposed old term read functions;

diff -r 1d8c6703c7b1 -r 1e9c05cddc64 NEWS
--- a/NEWS	Wed Jun 18 23:07:30 2008 +0200
+++ b/NEWS	Wed Jun 18 23:15:41 2008 +0200
@@ -61,6 +61,12 @@
 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,
+Syntax.read_term_global etc.; see also OldGoals.read_term as last
+resort for legacy applications.
+
 
 
 New in Isabelle2008 (June 2008)