# HG changeset patch
# User wenzelm
# Date 1683059587 -7200
# Node ID 948f5dc4d694a6350ff0e3f81d5ae75e674f2b4d
# Parent  c4677a6aae2c717bb7e74a523749e0a302f7fd3f
more complete accesses for hide operation (amending fcd85e04a948), e.g. relevant for AFP/thys/Jordan_Normal_Form/Matrix_Kernel.thy in AFP/4d8afd37b465;

diff -r c4677a6aae2c -r 948f5dc4d694 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue May 02 19:49:17 2023 +0200
+++ b/src/Pure/General/name_space.ML	Tue May 02 22:33:07 2023 +0200
@@ -160,8 +160,26 @@
 
 fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
 
+fun accesses ((_: string, mandatory) :: rest) =
+      let
+        val suppr = not mandatory;
+        val accs0 = accesses rest;
+        val accs1 = map (cons suppr) accs0;
+        val accs2 = if suppr then map (cons false) accs0 else [];
+      in accs1 @ accs2 end
+  | accesses [] = [[]];
+
 in
 
+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;
+
 fun make_accesses ({restriction, spec, ...}: Binding.name_spec) =
   if restriction = SOME true then []
   else
@@ -511,7 +529,7 @@
   space |> map_name_space (fn (kind, internals, entries, aliases) =>
     let
       val _ = the_entry space name;
-      val accesses = get_aliases space name |> maps (make_accesses o Binding.full_name_spec);
+      val accesses = get_aliases space name |> maps (make_accesses'' o Binding.full_name_spec);
       val accesses' = make_accesses' name;
       val xnames = filter (is_valid_access space name) accesses;
       val xnames' =