# HG changeset patch
# User wenzelm
# Date 1681420119 -7200
# Node ID de97fcc2c6243f70f2a31673ccc5c4d87414b9b5
# Parent  33d366e660617f5406ba2919c62ddbefca4c30c7
clarified signature;

diff -r 33d366e66061 -r de97fcc2c624 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Wed Apr 12 15:22:52 2023 +0200
+++ b/src/Pure/General/binding.ML	Thu Apr 13 23:08:39 2023 +0200
@@ -43,7 +43,7 @@
   val bad: binding -> string
   val check: binding -> unit
   val name_spec: scope list -> (string * bool) list -> binding ->
-    {restriction: bool option, concealed: bool, spec: (string * bool) list}
+    {restriction: bool option, concealed: bool, spec: (string * bool) list, full_name: string}
 end;
 
 structure Binding: BINDING =
@@ -211,8 +211,10 @@
     val _ =
       exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
       andalso error (bad binding);
-  in {restriction = restriction, concealed = concealed, spec = if null spec2 then [] else spec} end;
 
+    val spec' = if null spec2 then [] else spec;
+    val full_name = Long_Name.implode (map #1 spec');
+  in {restriction = restriction, concealed = concealed, spec = spec', full_name = full_name} end;
 
 end;
 
diff -r 33d366e66061 -r de97fcc2c624 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Apr 12 15:22:52 2023 +0200
+++ b/src/Pure/General/name_space.ML	Thu Apr 13 23:08:39 2023 +0200
@@ -428,10 +428,8 @@
 fun name_spec naming binding =
   Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding);
 
-fun full_name naming =
-  name_spec naming #> #spec #> map #1 #> Long_Name.implode;
-
-val base_name = full_name global_naming #> Long_Name.base_name;
+val full_name = #full_name oo name_spec;
+val base_name = Long_Name.base_name o full_name global_naming;
 
 
 (* accesses *)
@@ -450,14 +448,17 @@
 in
 
 fun make_accesses naming binding =
-  (case name_spec naming binding of
-    {restriction = SOME true, ...} => ([], [])
-  | {restriction, spec, ...} =>
-      let
-        val restrict = is_some restriction ? filter (fn [_] => false | _ => true);
-        val sfxs = restrict (mandatory_suffixes spec);
-        val pfxs = restrict (mandatory_prefixes spec);
-      in apply2 (map Long_Name.implode o distinct op =) (sfxs @ pfxs, sfxs) end);
+  let
+    val args as {restriction, spec, ...} = name_spec naming binding;
+    val accesses =
+      if restriction = SOME true then ([], [])
+      else
+        let
+          val restrict = is_some restriction ? filter (fn [_] => false | _ => true);
+          val sfxs = restrict (mandatory_suffixes spec);
+          val pfxs = restrict (mandatory_prefixes spec);
+        in apply2 (map Long_Name.implode o distinct op =) (sfxs @ pfxs, sfxs) end;
+  in (accesses, args) end;
 
 end;
 
@@ -487,7 +488,7 @@
   space |> map_name_space (fn (kind, internals, externals) =>
     let
       val _ = the_entry space name;
-      val (more_accs, more_accs') = make_accesses naming binding;
+      val (more_accs, more_accs') = #1 (make_accesses naming binding);
       val internals' = internals |> fold (add_name name) more_accs;
       val externals' = externals
         |> Change_Table.map_entry name (fn {accesses, accesses', entry} =>
@@ -529,10 +530,7 @@
   let
     val naming = naming_of context;
     val Naming {group, theory_long_name, ...} = naming;
-    val {concealed, spec, ...} = name_spec naming binding;
-    val (accesses, accesses') = make_accesses naming binding;
-
-    val name = Long_Name.implode (map fst spec);
+    val ((accesses, accesses'), {concealed, full_name = name, ...}) = make_accesses naming binding;
     val _ = name = "" andalso error (Binding.bad binding);
 
     val (proper_pos, pos) = Position.default (Binding.pos_of binding);