# HG changeset patch
# User wenzelm
# Date 1427909488 -7200
# Node ID 91f4f956b1eb59776eacafcdec59ba445670b869
# Parent  81c70bdbd908d9c2187d25af4189364da67eee34
NEWS;

diff -r 81c70bdbd908 -r 91f4f956b1eb NEWS
--- a/NEWS	Wed Apr 01 18:22:55 2015 +0200
+++ b/NEWS	Wed Apr 01 19:31:28 2015 +0200
@@ -329,6 +329,14 @@
 
 *** ML ***
 
+* Subtle change of name space policy: undeclared entries are now
+considered inaccessible, instead of accessible via the fully-qualified
+internal name. This mainly affects Name_Space.intern (and derivatives),
+which may produce an unexpected Long_Name.hidden prefix. Note that
+contempory applications use the strict Name_Space.check (and
+derivatives) instead, which is not affected by the change. Potential
+INCOMPATIBILITY in rare applications of Name_Space.intern.
+
 * The main operations to certify logical entities are Thm.ctyp_of and
 Thm.cterm_of with a local context; old-style global theory variants are
 available as Thm.global_ctyp_of and Thm.global_cterm_of.