# HG changeset patch
# User wenzelm
# Date 1683015182 -7200
# Node ID 81e356fd6f60628a0d3b6b99495877dc2b6c0996
# Parent  238307775d52acd76704fd86673bf59babba28d9
tuned;

diff -r 238307775d52 -r 81e356fd6f60 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon May 01 22:47:51 2023 +0200
+++ b/src/Pure/General/name_space.ML	Tue May 02 10:13:02 2023 +0200
@@ -129,8 +129,10 @@
 type internal = string list * string list;  (*visible, hidden*)
 type internals = internal Long_Name.Chunks.T;  (*xname -> internal*)
 
+val internal_default: internal = ([], []);
+
 fun map_internals f xname : internals -> internals =
-  Long_Name.Chunks.map_default (xname, ([], [])) f;
+  Long_Name.Chunks.map_default (xname, internal_default) f;
 
 val del_name = map_internals o apfst o remove (op =);
 fun del_name_extra name =
@@ -225,7 +227,7 @@
 (* intern *)
 
 fun intern_chunks space xname =
-  (case the_default ([], []) (lookup_internals space xname) of
+  (case the_default internal_default (lookup_internals space xname) of
     (name :: rest, _) => {name = name, full_name = name, unique = null rest}
   | ([], name' :: _) => {name = Long_Name.hidden name', full_name = "", unique = true}
   | _ => {name = Long_Name.hidden (Long_Name.implode_chunks xname), full_name = "", unique = true});