# HG changeset patch
# User wenzelm
# Date 1117696376 -7200
# Node ID 22324687e2d2506f60e34d12eee1eb3d0d211168
# Parent  a51be5cbd81d382db2c1a42a7ace6fb487136231
tuned;

diff -r a51be5cbd81d -r 22324687e2d2 NEWS
--- a/NEWS	Thu Jun 02 09:11:34 2005 +0200
+++ b/NEWS	Thu Jun 02 09:12:56 2005 +0200
@@ -425,8 +425,10 @@
   produce a fully qualified name and external accesses of a fully
   qualified name; NameSpace.extend is superceded by context dependent
   Sign.declare_name.  Several theory and proof context operations
-  modify the naming context; especially note Theory.restore_naming and
-  ProofContext.restore_naming.
+  modify the naming context.  Especially note Theory.restore_naming
+  and ProofContext.restore_naming to get back to a sane state; note
+  that Theory.add_path is no longer sufficient to recover from
+  Theory.absolute_path in particular.
 
 * Pure: cases produced by proof methods specify options, where NONE
   means to remove case bindings -- INCOMPATIBILITY in