--- a/NEWS Mon Oct 08 22:06:32 2007 +0200
+++ b/NEWS Tue Oct 09 00:20:13 2007 +0200
@@ -1307,6 +1307,13 @@
(Syntax.read_term etc.). These supersede former Sign.read_term etc.
which are considered legacy and await removal.
+* Pure/Syntax: generic interfaces for type unchecking
+(Syntax.uncheck_terms etc.) and unparsing (Syntax.unparse_term etc.),
+with common combinations (Syntax.pretty_term, Syntax.string_of_term
+etc.). Former Sign.pretty_term, Sign.string_of_term etc. are still
+available for convenience, but refer to the very same operations
+(using a mere theory instead of a full context).
+
* Isar: simplified treatment of user-level errors, using exception
ERROR of string uniformly. Function error now merely raises ERROR,
without any side effect on output channels. The Isar toplevel takes