# HG changeset patch
# User wenzelm
# Date 1683281849 -7200
# Node ID 8ce2425a7c94dc9adaa9be04c1c83ff3c3e545d3
# Parent  6bb2f9b3280498a0b4c1a98fbc0f461c0b4ef9e4
tuned;

diff -r 6bb2f9b32804 -r 8ce2425a7c94 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri May 05 12:01:09 2023 +0200
+++ b/src/Pure/General/name_space.ML	Fri May 05 12:17:29 2023 +0200
@@ -224,14 +224,17 @@
 
 fun get_accesses {intern, aliases} space name =
   let
-    fun suppress a =
-      (case lookup_entries space a of
-        SOME {suppress, ...} => suppress
-      | NONE => []);
     fun accesses a =
-      make_accesses {intern = intern} NONE (suppress a) a
-      |> filter (is_valid_access space a);
-  in maps accesses (if aliases then get_aliases space name else [name]) end;
+      let
+        val suppress =
+          (case lookup_entries space a of
+            SOME {suppress, ...} => suppress
+          | NONE => [])
+      in
+        make_accesses {intern = intern} NONE suppress a
+        |> filter (is_valid_access space a)
+      end;
+  in if aliases then maps accesses (get_aliases space name) else accesses name end;
 
 fun gen_markup def space name =
   (case lookup_entries space name of