# HG changeset patch
# User wenzelm
# Date 1427829142 -7200
# Node ID 3470a265d404d85f3441c8bab976a0295fe54f7b
# Parent  bbf49d7dfd6f2c8ef8ab71e7489e48415b7bad74
subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;

diff -r bbf49d7dfd6f -r 3470a265d404 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Tue Mar 31 20:18:10 2015 +0200
+++ b/src/Pure/General/binding.ML	Tue Mar 31 21:12:22 2015 +0200
@@ -47,7 +47,7 @@
 (* datatype *)
 
 datatype binding = Binding of
- {private: bool,                    (*entry is private -- no name space accesses, only full name*)
+ {private: bool,                    (*entry is strictly private -- no name space accesses*)
   concealed: bool,                  (*entry is for foundational purposes -- please ignore*)
   prefix: (string * bool) list,     (*system prefix*)
   qualifier: (string * bool) list,  (*user qualifier*)
diff -r bbf49d7dfd6f -r 3470a265d404 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Mar 31 20:18:10 2015 +0200
+++ b/src/Pure/General/name_space.ML	Tue Mar 31 21:12:22 2015 +0200
@@ -166,18 +166,17 @@
 (* intern *)
 
 fun intern' (Name_Space {internals, ...}) xname =
-  (case Change_Table.lookup internals xname of
-    NONE => (xname, true)
-  | SOME ([], []) => (xname, true)
-  | SOME ([name], _) => (name, true)
-  | SOME (name :: _, _) => (name, false)
-  | SOME ([], name' :: _) => (Long_Name.hidden name', true));
+  (case the_default ([], []) (Change_Table.lookup internals xname) of
+    ([name], _) => (name, true)
+  | (name :: _, _) => (name, false)
+  | ([], []) => (Long_Name.hidden xname, true)
+  | ([], name' :: _) => (Long_Name.hidden name', true));
 
 val intern = #1 oo intern';
 
 fun get_accesses (Name_Space {entries, ...}) name =
   (case Change_Table.lookup entries name of
-    NONE => [name]
+    NONE => []
   | SOME (externals, _) => externals);
 
 fun valid_accesses (Name_Space {internals, ...}) name =
diff -r bbf49d7dfd6f -r 3470a265d404 src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Mar 31 20:18:10 2015 +0200
+++ b/src/Pure/type.ML	Tue Mar 31 21:12:22 2015 +0200
@@ -659,8 +659,9 @@
   let
     val types' = f types;
     val _ =
+      not (Name_Space.defined types' "dummy") orelse
       Name_Space.intern (Name_Space.space_of_table types') "dummy" = "dummy" orelse
-        error "Illegal declaration of dummy type";
+      error "Illegal declaration of dummy type";
   in (classes, default, types') end);
 
 fun syntactic tsig (Type (c, Ts)) =