tuned;
authorwenzelm
Fri, 05 May 2023 12:17:29 +0200
changeset 77968 8ce2425a7c94
parent 77967 6bb2f9b32804
child 77969 f68df517e8c4
tuned;
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