# 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