* HOL: syntax translations now work properly with numerals and records
expressions;

--- a/NEWS	Wed Aug 08 16:57:43 2001 +0200
+++ b/NEWS	Wed Aug 08 17:37:47 2001 +0200
@@ -21,8 +21,8 @@
   relations has too general a domain, namely ('a * 'b)set and 'a => 'b.
   This means that it may be necessary to attach explicit type constraints.
 
-* HOL records: fix problem with user translations by making field
-names appear as syntactic conststants;
+* HOL: syntax translations now work properly with numerals and records
+expressions;
 
 * HOL/GroupTheory: group theory examples including Sylow's theorem, by
 Florian Kammüller;