HOL/record: shared operations ("more", "fields", etc.) now need to be
always qualified;

--- a/NEWS	Fri Dec 21 20:58:42 2001 +0100
+++ b/NEWS	Fri Dec 21 23:16:17 2001 +0100
@@ -190,6 +190,8 @@
     "extend" to promote a fixed record to a record scheme, and
     "truncate" for the reverse; cf. theorems "xxx.defs", which are *not*
     declared as simp by default;
+  - shared operations ("more", "fields", etc.) now need to be always
+    qualified) --- potential INCOMPATIBILITY;
   - removed "make_scheme" operations (use "make" with "extend") --
     INCOMPATIBILITY;
   - removed "more" class (simply use "term") -- INCOMPATIBILITY;