diff -r 81e356fd6f60 -r 0290a9879b03 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Tue May 02 10:13:02 2023 +0200
+++ b/src/Pure/General/binding.ML	Tue May 02 10:30:03 2023 +0200
@@ -42,8 +42,9 @@
   val print: binding -> string
   val bad: binding -> string
   val check: binding -> unit
-  val name_spec: scope list -> (string * bool) list -> binding ->
+  type name_spec =
     {restriction: bool option, concealed: bool, spec: (string * bool) list, full_name: string}
+  val name_spec: scope list -> (string * bool) list -> binding -> name_spec
 end;
 
 structure Binding: BINDING =
@@ -194,7 +195,10 @@
 
 val bad_specs = ["", "??", "__"];
 
-fun name_spec scopes path binding =
+type name_spec =
+  {restriction: bool option, concealed: bool, spec: (string * bool) list, full_name: string};
+
+fun name_spec scopes path binding : name_spec =
   let
     val Binding {restricted, concealed, prefix, qualifier, name, ...} = binding;
     val _ = Long_Name.is_qualified name andalso error (bad binding);