# HG changeset patch
# User wenzelm
# Date 1681291631 -7200
# Node ID 29146fb57e791fc6243bbe3960c8d90f24e038b5
# Parent  56d7da3e79feaa6a76e447b6455ee4d0b02fb377
tuned;

diff -r 56d7da3e79fe -r 29146fb57e79 src/Pure/General/name_space.ML
--- 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 *)