--- a/src/Pure/General/name_space.ML Wed Apr 12 11:25:50 2023 +0200
+++ b/src/Pure/General/name_space.ML Wed Apr 12 11:27:11 2023 +0200
@@ -435,6 +435,8 @@
(* accesses *)
+local
+
fun mandatory xs = fold_rev (fn (x, b) => b ? cons x) xs [];
fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
@@ -444,6 +446,8 @@
fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
+in
+
fun make_accesses naming binding =
(case name_spec naming binding of
{restriction = SOME true, ...} => ([], [])
@@ -454,6 +458,8 @@
val pfxs = restrict (mandatory_prefixes spec);
in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
+end;
+
(* hide *)