# HG changeset patch
# User wenzelm
# Date 1683106487 -7200
# Node ID d7eabea9f837c1efbedd1ac98b8dbd0994e94f74
# Parent  fda3e9c8a894e2ce051708fa6bb29a205614b2fb
proper treatment of restriction (for 'qualified');
tuned;

diff -r fda3e9c8a894 -r d7eabea9f837 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue May 02 23:22:30 2023 +0200
+++ b/src/Pure/General/name_space.ML	Wed May 03 11:34:47 2023 +0200
@@ -174,11 +174,16 @@
 fun make_accesses'' ({restriction, spec, full_name, ...}: Binding.name_spec) =
   if restriction = SOME true then []
   else
-    accesses spec
-    |> restriction = SOME false ? filter (fn [_] => false | _ => true)
-    |> map (fn s => Long_Name.suppress_chunks 0 s full_name)
-    |> remove Long_Name.eq_chunks Long_Name.empty_chunks
-    |> distinct Long_Name.eq_chunks;
+    let
+      val m = if is_some restriction then 1 else 0;
+      fun make_chunks s =
+        let val chunks = Long_Name.suppress_chunks 0 s full_name
+        in if Long_Name.count_chunks chunks > m then SOME chunks else NONE end;
+    in
+      accesses spec
+      |> map_filter make_chunks
+      |> distinct Long_Name.eq_chunks
+    end;
 
 fun make_accesses ({restriction, spec, ...}: Binding.name_spec) =
   if restriction = SOME true then []