changeset 59899 91f4f956b1eb
parent 59892 2a616319c171
child 59901 840d03805755
--- 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.