src/Pure/General/binding.ML

--- a/src/Pure/General/binding.ML	Wed May 03 23:11:12 2023 +0200
+++ b/src/Pure/General/binding.ML	Thu May 04 11:42:04 2023 +0200
@@ -43,9 +43,8 @@
   val bad: binding -> string
   val check: binding -> unit
   type name_spec =
-    {restriction: bool option, concealed: bool, spec: (string * bool) list, full_name: string}
+    {restriction: bool option, concealed: bool, suppress: bool list, full_name: string}
   val name_spec: scope list -> (string * bool) list -> binding -> name_spec
-  val full_name_spec: string -> name_spec
 end;
 
 structure Binding: BINDING =
@@ -197,7 +196,7 @@
 val bad_specs = ["", "??", "__"];
 
 type name_spec =
-  {restriction: bool option, concealed: bool, spec: (string * bool) list, full_name: string};
+  {restriction: bool option, concealed: bool, suppress: bool list, full_name: string};
 
 fun name_spec scopes path binding : name_spec =
   let
@@ -218,12 +217,11 @@
       andalso error (bad binding);
 
     val spec' = if null spec2 then [] else spec;
+    val suppress = map (not o #2) spec';
     val full_name = Long_Name.implode (map #1 spec');
-  in {restriction = restriction, concealed = concealed, spec = spec', full_name = full_name} end;
-
-fun full_name_spec name : name_spec =
-  let val spec = Long_Name.explode name |> map (rpair false);
-  in {restriction = NONE, concealed = false, spec = spec, full_name = name} end;
+  in
+    {restriction = restriction, concealed = concealed, suppress = suppress, full_name = full_name}
+  end;
 
 end;