--- a/src/Pure/General/name_space.ML Sat May 06 14:46:41 2023 +0200
+++ b/src/Pure/General/name_space.ML Sat May 06 14:49:54 2023 +0200
@@ -148,13 +148,13 @@
val merge_internals : internals * internals -> internals = Long_Name.Chunks.merge_list (op =);
-fun add_name name xname : internals -> internals =
+fun add_internals name xname : internals -> internals =
Long_Name.Chunks.update_list (op =) (xname, name);
-fun del_name name xname : internals -> internals =
+fun del_internals name xname : internals -> internals =
Long_Name.Chunks.remove_list (op =) (xname, name);
-fun del_name_extra name xname : internals -> internals =
+fun del_internals' name xname : internals -> internals =
Long_Name.Chunks.map_default (xname, []) (fn [] => [] | x :: xs => x :: remove (op =) name xs);
@@ -541,10 +541,10 @@
|> not fully ? inter Long_Name.eq_chunks [Long_Name.base_chunks name];
val accesses' = get_accesses {intern = false, aliases = false, valid = true} space name;
val internals' = internals
- |> fold (del_name name) accesses
- |> fold (del_name_extra name) accesses';
+ |> fold (del_internals name) accesses
+ |> fold (del_internals' name) accesses';
val internals_hidden' = internals_hidden
- |> add_name name (Long_Name.make_chunks name);
+ |> add_internals name (Long_Name.make_chunks name);
in (kind, internals', internals_hidden', entries, aliases) end);
@@ -561,7 +561,7 @@
in
space |> map_name_space (fn (kind, internals, internals_hidden, entries, aliases) =>
let
- val internals' = internals |> fold (add_name name) alias_accesses;
+ val internals' = internals |> fold (add_internals name) alias_accesses;
val entries' =
if name <> alias_name andalso (new_entry orelse strict) then
entries |> update_entry strict kind (alias_name,
@@ -624,7 +624,7 @@
val space' =
space |> map_name_space (fn (kind, internals, internals_hidden, entries, aliases) =>
let
- val internals' = internals |> fold (add_name name) accesses;
+ val internals' = internals |> fold (add_internals name) accesses;
val entries' = entries |> update_entry strict kind (name, entry);
in (kind, internals', internals_hidden, entries', aliases) end);
val _ =