subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
--- 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*)
--- 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 =
--- 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)) =