merged

--- a/NEWS	Sun May 07 14:52:53 2023 +0100
+++ b/NEWS	Sun May 07 22:51:23 2023 +0200
@@ -7,6 +7,17 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* The special "of_class" introduction rule for 'class' definitions has
+been renamed from "class.NAME.of_class.intro" to "NAME.intro_of_class"
+(where NAME is the name specification of the class). E.g. see the HOL
+library:
+
+  class.preorder.of_class.intro  ~>  preorder.intro_of_class
+  class.order.of_class.intro  ~> order.intro_of_class
+
+
 *** Document preparation ***
 
 * Various well-known LaTeX styles are included as Isabelle components,

--- a/src/HOL/Library/Lexord.thy	Sun May 07 14:52:53 2023 +0100
+++ b/src/HOL/Library/Lexord.thy	Sun May 07 22:51:23 2023 +0200
@@ -153,7 +153,7 @@
     and less_list = lex.lex_less ..
 
 instance
-  by (rule class.preorder.of_class.intro, rule preordering_preorderI, fact lex.preordering)
+  by (rule preorder.intro_of_class, rule preordering_preorderI, fact lex.preordering)
 
 end
 
@@ -171,7 +171,7 @@
 qed
 
 instance list :: (order) order
-  by (rule class.order.of_class.intro, rule ordering_orderI, fact lex.ordering)
+  by (rule order.intro_of_class, rule ordering_orderI, fact lex.ordering)
 
 export_code \<open>(\<le>) :: _ list \<Rightarrow> _ list \<Rightarrow> bool\<close> \<open>(<) :: _ list \<Rightarrow> _ list \<Rightarrow> bool\<close> in Haskell
 

--- a/src/HOL/Library/Poly_Mapping.thy	Sun May 07 14:52:53 2023 +0100
+++ b/src/HOL/Library/Poly_Mapping.thy	Sun May 07 22:51:23 2023 +0200
@@ -910,7 +910,7 @@
   is "\<lambda>f g. less_fun f g \<or> f = g"
   .
 
-instance proof (rule class.Orderings.linorder.of_class.intro)
+instance proof (rule linorder.intro_of_class)
   show "class.linorder (less_eq :: (_ \<Rightarrow>\<^sub>0 _) \<Rightarrow> _) less"
   proof (rule linorder_strictI, rule order_strictI)
     fix f g h :: "'a \<Rightarrow>\<^sub>0 'b"

--- a/src/Pure/General/binding.ML	Sun May 07 14:52:53 2023 +0100
+++ b/src/Pure/General/binding.ML	Sun May 07 22:51:23 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 ->
-    {restriction: bool option, concealed: bool, spec: (string * bool) list, full_name: string}
+  type name_spec =
+    {restriction: bool option, concealed: bool, suppress: 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, suppress: 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);
@@ -213,8 +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;
+  in
+    {restriction = restriction, concealed = concealed, suppress = suppress, full_name = full_name}
+  end;
 
 end;
 

--- a/src/Pure/General/change_table.ML	Sun May 07 14:52:53 2023 +0100
+++ b/src/Pure/General/change_table.ML	Sun May 07 22:51:23 2023 +0200
@@ -30,6 +30,11 @@
   val map_entry: key -> ('a -> 'a) -> 'a T -> 'a T
   val map_default: key * 'a -> ('a -> 'a) -> 'a T -> 'a T
   val delete_safe: key -> 'a T -> 'a T
+  val lookup_list: 'a list T -> Table.key -> 'a list
+  val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list T -> 'a list T
+  val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list T -> 'a list T
+  val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list T -> 'a list T
+  val merge_list: ('a * 'a -> bool) -> 'a list T * 'a list T -> 'a list T
 end;
 
 functor Change_Table(Key: KEY): CHANGE_TABLE =
@@ -135,6 +140,9 @@
 fun merge eq =
   join (fn key => fn xy => if eq xy then raise Table.SAME else raise Table.DUP key);
 
+fun merge_list eq =
+  join (fn _ => fn xy => if eq_list eq xy then raise Table.SAME else Library.merge eq xy);
+
 
 (* derived operations *)
 
@@ -153,7 +161,11 @@
 fun map_default (key, x) f = change_table key (Table.map_default (key, x) f);
 fun delete_safe key        = change_table key (Table.delete_safe key);
 
+fun lookup_list arg = Table.lookup_list (table_of arg);
+fun insert_list eq (key, x) = change_table key (Table.insert_list eq (key, x));
+fun remove_list eq (key, x) = change_table key (Table.remove_list eq (key, x));
+fun update_list eq (key, x) = change_table key (Table.update_list eq (key, x));
+
 end;
 
 structure Change_Table = Change_Table(type key = string val ord = fast_string_ord);
-

--- a/src/Pure/General/long_name.ML	Sun May 07 14:52:53 2023 +0100
+++ b/src/Pure/General/long_name.ML	Sun May 07 22:51:23 2023 +0200
@@ -25,12 +25,13 @@
   val count_chunks: chunks -> int
   val size_chunks: chunks -> int
   val empty_chunks: chunks
+  val is_empty_chunks: chunks -> bool
   val base_chunks: string -> chunks
   val suppress_chunks: int -> bool list -> string -> chunks
   val make_chunks: string -> chunks
   val explode_chunks: chunks -> string list
   val implode_chunks: chunks -> string
-  val compare_chunks: chunks * chunks -> order
+  val compare_chunks: chunks ord
   val eq_chunks: chunks * chunks -> bool
   structure Chunks: CHANGE_TABLE
 end;
@@ -107,18 +108,26 @@
 fun range_length r = r mod range_limit;
 fun range_string s r = String.substring (s, range_index r, range_length r);
 
+val range_empty = 0;
+val ranges_empty: int vector = Vector.fromList [];
+
 in
 
-abstype chunks = Chunks of {ranges: int list (*reverse*), string: string}
+abstype chunks = Chunks of {range0: int, ranges: int list (*reverse*), string: string}
 with
 
-fun count_chunks (Chunks {ranges, ...}) = length ranges;
+val empty_chunks = Chunks {range0 = range_empty, ranges = [], string = ""};
+
+fun is_empty_chunks (Chunks {range0, ranges, ...}) =
+  range0 = range_empty andalso null ranges;
 
-fun size_chunks (Chunks {ranges, ...}) =
-  if null ranges then 0
-  else fold (fn r => fn n => n + range_length r + 1) ranges ~1;
+fun count_chunks (chunks as Chunks {ranges, ...}) =
+  if is_empty_chunks chunks then 0
+  else length ranges + 1;
 
-val empty_chunks = Chunks {ranges = [], string = ""};
+fun size_chunks (chunks as Chunks {range0, ranges, ...}) =
+  if is_empty_chunks chunks then 0
+  else fold (fn r => fn n => n + range_length r + 1) ranges (range_length range0);
 
 fun base_chunks name =
   let
@@ -126,7 +135,7 @@
     val j = i + 1;
   in
     if i < 0 then empty_chunks
-    else Chunks {ranges = [range name j (size name - j)], string = name}
+    else Chunks {range0 = range name j (size name - j), ranges = [], string = name}
   end;
 
 fun suppress_chunks suppress1 suppress2 string =
@@ -158,25 +167,30 @@
         if not string_end then suppr_chunks suppr1' suppr2' i' j' rs'
         else if not (suppr1' = 0 andalso null suppr2') then
           failure string ("cannot suppress chunks beyond " ^ string_of_int (length rs'))
-        else if null rs' then empty_chunks
-        else Chunks {ranges = rs', string = string}
+        else
+          (case rs' of
+            [] => empty_chunks
+          | r0 :: rest => Chunks {range0 = r0, ranges = rest, string = string})
       end;
   in suppr_chunks suppress1 suppress2 0 0 [] end;
 
 val make_chunks = suppress_chunks 0 [];
 
-fun explode_chunks (Chunks {ranges, string}) =
-  fold (cons o range_string string) ranges [];
+fun explode_chunks (chunks as Chunks {range0, ranges, string}) =
+  if is_empty_chunks chunks then []
+  else fold (cons o range_string string) ranges [range_string string range0];
 
-fun implode_chunks (chunks as Chunks {ranges, string}) =
+fun implode_chunks (chunks as Chunks {range0, ranges, string}) =
   if size_chunks chunks = size string then string
-  else if length ranges = 1 then range_string string (nth ranges 0)
+  else if null ranges then range_string string range0
   else implode (explode_chunks chunks);
 
 val compare_chunks = pointer_eq_ord (fn (chunks1, chunks2) =>
   let
-    val Chunks {ranges = ranges1, string = string1} = chunks1;
-    val Chunks {ranges = ranges2, string = string2} = chunks2;
+    val Chunks {range0 = range01, ranges = ranges1, string = string1} = chunks1;
+    val Chunks {range0 = range02, ranges = ranges2, string = string2} = chunks2;
+    val count1 = count_chunks chunks1;
+    val count2 = count_chunks chunks2;
 
     val range_length_ord = int_ord o apply2 range_length;
     fun range_substring_ord arg =
@@ -192,9 +206,20 @@
           else EQUAL;
       in (case int_ord (m, n) of EQUAL => substring_ord 0 | ord => ord) end;
   in
-    (case list_ord range_length_ord (ranges1, ranges2) of
-      EQUAL => dict_ord range_substring_ord (ranges1, ranges2)
-    | ord => ord)
+    if count1 = 0 andalso count2 = 0 then EQUAL
+    else
+      (case int_ord (count1, count2) of
+        EQUAL =>
+          (case range_length_ord (range01, range02) of
+            EQUAL =>
+              (case dict_ord range_length_ord (ranges1, ranges2) of
+                EQUAL =>
+                  (case range_substring_ord (range01, range02) of
+                    EQUAL => dict_ord range_substring_ord (ranges1, ranges2)
+                  | ord => ord)
+              | ord => ord)
+          | ord => ord)
+      | ord => ord)
   end);
 
 val eq_chunks = is_equal o compare_chunks;

--- a/src/Pure/General/name_space.ML	Sun May 07 14:52:53 2023 +0100
+++ b/src/Pure/General/name_space.ML	Sun May 07 22:51:23 2023 +0200
@@ -1,28 +1,27 @@
 (*  Title:      Pure/General/name_space.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
-Generic name spaces with declared and hidden entries; no support for
-absolute addressing.
+Generic name spaces with authentic declarations, hidden names and aliases.
 *)
 
-type xstring = string;    (*external names*)
+type xstring = string;    (*external names with partial qualification*)
 
 signature NAME_SPACE =
 sig
-  type entry =
-   {concealed: bool,
-    group: serial,
-    theory_long_name: string,
-    pos: Position.T,
-    serial: serial}
   type T
   val empty: string -> T
   val kind_of: T -> string
   val markup: T -> string -> Markup.T
   val markup_def: T -> string -> Markup.T
   val get_names: T -> string list
-  val the_entry: T -> string -> entry
-  val the_entry_theory_name: T -> string -> string
+  val the_entry: T -> string ->
+   {concealed: bool,
+    suppress: bool list,
+    group: serial,
+    theory_long_name: string,
+    pos: Position.T,
+    serial: serial}
+  val theory_name: {long: bool} -> T -> string -> string
   val entry_ord: T -> string ord
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
@@ -108,103 +107,160 @@
 
 type entry =
  {concealed: bool,
+  suppress: bool list,
   group: serial,
   theory_long_name: string,
   pos: Position.T,
   serial: serial};
 
-fun entry_markup def kind (name, {pos, serial, ...}: entry) =
-  Position.make_entity_markup def serial kind (name, pos);
+fun markup_entry def kind (name, entry: entry) =
+  Position.make_entity_markup def (#serial entry) kind (name, #pos entry);
 
 fun print_entry_ref kind (name, entry) =
-  quote (Markup.markup (entry_markup {def = false} kind (name, entry)) name);
+  quote (Markup.markup (markup_entry {def = false} kind (name, entry)) name);
 
-fun err_dup kind entry1 entry2 pos =
+fun err_dup_entry kind entry1 entry2 pos =
   error ("Duplicate " ^ plain_words kind ^ " declaration " ^
     print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos);
 
+fun update_entry strict kind (name, entry: entry) entries =
+  (if strict then Change_Table.update_new else Change_Table.update) (name, entry) entries
+    handle Change_Table.DUP _ =>
+      let val old_entry = the (Change_Table.lookup entries name)
+      in err_dup_entry kind (name, old_entry) (name, entry) (#pos entry) end;
+
 
 (* internal names *)
 
-type internal = string list * string list;  (*visible, hidden*)
-type internals = internal Long_Name.Chunks.T;  (*xname -> internal*)
+type internals = string list Long_Name.Chunks.T;  (*external name -> internal names*)
 
-fun map_internals f xname : internals -> internals =
-  Long_Name.Chunks.map_default (xname, ([], [])) f;
+val merge_internals : internals * internals -> internals = Long_Name.Chunks.merge_list (op =);
 
-val del_name = map_internals o apfst o remove (op =);
-fun del_name_extra name =
-  map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
-val add_name = map_internals o apfst o update (op =);
-fun hide_name name = map_internals (apsnd (update (op =) name)) (Long_Name.make_chunks name);
+fun add_internals name xname : internals -> internals =
+  Long_Name.Chunks.update_list (op =) (xname, name);
+
+fun del_internals name xname : internals -> internals =
+  Long_Name.Chunks.remove_list (op =) (xname, name);
+
+fun del_internals' name xname : internals -> internals =
+  Long_Name.Chunks.map_default (xname, []) (fn [] => [] | x :: xs => x :: remove (op =) name xs);
 
 
-(* external accesses *)
+(* accesses *)
+
+local
+
+fun suppress_prefixes1 [] = []
+  | suppress_prefixes1 (s :: ss) =
+      map (cons false) (if s then suppress_prefixes ss else suppress_prefixes1 ss)
+and suppress_prefixes ss = ss :: suppress_prefixes1 ss;
+
+fun suppress_suffixes ss = map rev (suppress_prefixes (rev ss));
 
-type external =
- {accesses: Long_Name.chunks list,
-  accesses': Long_Name.chunks list,
-  entry: entry};
+fun make_chunks full_name m 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
 
-type externals = external Change_Table.T;  (*name -> external*)
+fun make_accesses {intern} restriction (suppress, full_name) =
+  if restriction = SOME true then []
+  else
+    ((if intern then suppress_prefixes suppress else []) @ suppress_suffixes suppress)
+    |> map_filter (make_chunks full_name (if is_some restriction then 1 else 0))
+    |> distinct Long_Name.eq_chunks;
+
+end;
 
 
 (* datatype T *)
 
-datatype T = Name_Space of {kind: string, internals: internals, externals: externals};
+datatype T =
+  Name_Space of
+   {kind: string,
+    internals: internals,
+    internals_hidden: internals,
+    entries: entry Change_Table.T,
+    aliases: (bool list * string) list Symtab.table};
 
-fun make_name_space (kind, internals, externals) =
-  Name_Space {kind = kind, internals = internals, externals = externals};
+fun make_name_space (kind, internals, internals_hidden, entries, aliases) =
+  Name_Space {kind = kind, internals = internals, internals_hidden = internals_hidden,
+    entries = entries, aliases = aliases};
 
-fun map_name_space f (Name_Space {kind = kind, internals = internals, externals = externals}) =
-  make_name_space (f (kind, internals, externals));
+fun map_name_space f (Name_Space {kind, internals, internals_hidden, entries, aliases}) =
+  make_name_space (f (kind, internals, internals_hidden, entries, aliases));
 
-fun change_base_space begin = map_name_space (fn (kind, internals, externals) =>
-  (kind,
-    Long_Name.Chunks.change_base begin internals,
-    Change_Table.change_base begin externals));
+fun change_base_space begin =
+  map_name_space (fn (kind, internals, internals_hidden, entries, aliases) =>
+    (kind,
+      Long_Name.Chunks.change_base begin internals,
+      Long_Name.Chunks.change_base begin internals_hidden,
+      Change_Table.change_base begin entries,
+      aliases));
 
-val change_ignore_space = map_name_space (fn (kind, internals, externals) =>
-  (kind,
-    Long_Name.Chunks.change_ignore internals,
-    Change_Table.change_ignore externals));
+val change_ignore_space =
+  map_name_space (fn (kind, internals, internals_hidden, entries, aliases) =>
+    (kind,
+      Long_Name.Chunks.change_ignore internals,
+      Long_Name.Chunks.change_ignore internals_hidden,
+      Change_Table.change_ignore entries,
+      aliases));
 
 
-fun empty kind = make_name_space (kind, Long_Name.Chunks.empty, Change_Table.empty);
+fun empty kind =
+  make_name_space
+    (kind, Long_Name.Chunks.empty, Long_Name.Chunks.empty, Change_Table.empty, Symtab.empty);
 
 fun kind_of (Name_Space {kind, ...}) = kind;
-fun lookup_internals (Name_Space {internals, ...}) = Long_Name.Chunks.lookup internals;
-fun lookup_externals (Name_Space {externals, ...}) = Change_Table.lookup externals;
+fun lookup_internals (Name_Space {internals, ...}) =
+  Long_Name.Chunks.lookup_list internals;
+fun lookup_internals_hidden (Name_Space {internals_hidden, ...}) =
+  Long_Name.Chunks.lookup_list internals_hidden;
+fun lookup_entries (Name_Space {entries, ...}) = Change_Table.lookup entries;
+fun lookup_aliases (Name_Space {aliases, ...}) = Symtab.lookup_list aliases;
+
+
+fun suppress_entry space name =
+  (case lookup_entries space name of
+    SOME {suppress, ...} => (suppress, name)
+  | NONE => ([], name));
+
+fun is_alias space c a =
+  c = a orelse exists (fn (_, b) => b = a) (lookup_aliases space c);
+
+fun get_aliases space name =
+  lookup_aliases space name @ [suppress_entry space name];
 
 fun gen_markup def space name =
-  (case lookup_externals space name of
+  (case lookup_entries space name of
     NONE => Markup.intensify
-  | SOME {entry, ...} => entry_markup def (kind_of space) (name, entry));
+  | SOME entry => markup_entry def (kind_of space) (name, entry));
 
 val markup = gen_markup {def = false};
 val markup_def = gen_markup {def = true};
 
-fun undefined (space as Name_Space {kind, externals, ...}) bad =
+fun undefined_entry (space as Name_Space {kind, entries, ...}) bad =
   let
     val (prfx, sfx) =
       (case Long_Name.dest_hidden bad of
         SOME name =>
-          if Change_Table.defined externals name
+          if Change_Table.defined entries name
           then ("Inaccessible", Markup.markup (markup space name) (quote name))
           else ("Undefined", quote name)
       | NONE => ("Undefined", quote bad));
   in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end;
 
-fun get_names (Name_Space {externals, ...}) =
-  Change_Table.fold (cons o #1) externals [];
+fun the_entry space name =
+  (case lookup_entries space name of
+    SOME entry => entry
+  | _ => error (undefined_entry space name));
 
-fun the_entry space name =
-  (case lookup_externals space name of
-    NONE => error (undefined space name)
-  | SOME {entry, ...} => entry);
+fun get_names (Name_Space {entries, ...}) =
+  Change_Table.fold (cons o #1) entries [];
 
-fun the_entry_theory_name space name =
-  Long_Name.base_name (#theory_long_name (the_entry space name));
+fun theory_name {long} space name =
+  #theory_long_name (the_entry space name)
+  |> not long ? Long_Name.base_name;
 
 fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
 
@@ -215,18 +271,17 @@
 (* intern *)
 
 fun intern_chunks space xname =
-  (case the_default ([], []) (lookup_internals space xname) of
-    ([name], _) => (name, true)
-  | (name :: _, _) => (name, false)
-  | ([], []) => (Long_Name.hidden (Long_Name.implode_chunks xname), true)
-  | ([], name' :: _) => (Long_Name.hidden name', true));
+  (case lookup_internals space xname of
+    name :: rest => {name = name, full_name = name, unique = null rest}
+  | [] =>
+      (case lookup_internals_hidden space xname of
+        name' :: _ => {name = Long_Name.hidden name', full_name = "", unique = true}
+      | [] =>
+         {name = Long_Name.hidden (Long_Name.implode_chunks xname),
+          full_name = "",
+          unique = true}));
 
-fun intern space = #1 o intern_chunks space o Long_Name.make_chunks;
-
-fun is_valid_access space name xname =
-  (case lookup_internals space xname of
-    SOME (name' :: _, _) => name = name'
-  | _ => false);
+fun intern space = #name o intern_chunks space o Long_Name.make_chunks;
 
 
 (* extern *)
@@ -241,23 +296,28 @@
     val names_short = Config.get ctxt names_short;
     val names_unique = Config.get ctxt names_unique;
 
-    fun valid require_unique xname =
-      let val (name', is_unique) = intern_chunks space xname
-      in name = name' andalso (not require_unique orelse is_unique) end;
+    fun extern_chunks require_unique a chunks =
+      let val {full_name = c, unique, ...} = intern_chunks space chunks in
+        if (not require_unique orelse unique) andalso is_alias space c a
+        then SOME (Long_Name.implode_chunks chunks)
+        else NONE
+      end;
 
-    fun extern [] =
-          if valid false (Long_Name.make_chunks name) then name
-          else Long_Name.hidden name
-      | extern (a :: bs) =
-          if valid names_unique a then Long_Name.implode_chunks a
-          else extern bs;
+    fun extern_name (suppress, a) =
+      get_first (extern_chunks names_unique a)
+        (make_accesses {intern = false} NONE (suppress, a));
+
+    fun extern_names aliases =
+      (case get_first extern_name aliases of
+        SOME xname => xname
+      | NONE =>
+          (case get_first (fn (_, a) => extern_chunks false a (Long_Name.make_chunks a)) aliases of
+            SOME xname => xname
+          | NONE => Long_Name.hidden name));
   in
     if names_long then name
     else if names_short then Long_Name.base_name name
-    else
-      (case lookup_externals space name of
-        NONE => extern []
-      | SOME {accesses', ...} => extern accesses')
+    else extern_names (get_aliases space name)
   end;
 
 fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space);
@@ -306,7 +366,7 @@
         else I;
     in
       Long_Name.Chunks.fold
-        (fn (xname', (name :: _, _)) => complete (Long_Name.implode_chunks xname') name | _ => I)
+        (fn (xname', name :: _) => complete (Long_Name.implode_chunks xname') name | _ => I)
         internals []
       |> sort_distinct result_ord
       |> map #2
@@ -316,23 +376,22 @@
 (* merge *)
 
 fun merge
-  (Name_Space {kind = kind1, internals = internals1, externals = externals1},
-    Name_Space {kind = kind2, internals = internals2, externals = externals2}) =
+   (Name_Space {kind = kind1, internals = internals1, internals_hidden = internals_hidden1,
+     entries = entries1, aliases = aliases1},
+    Name_Space {kind = kind2, internals = internals2, internals_hidden = internals_hidden2,
+     entries = entries2, aliases = aliases2}) =
   let
     val kind' =
       if kind1 = kind2 then kind1
       else error ("Attempt to merge different kinds of name spaces " ^
         quote kind1 ^ " vs. " ^ quote kind2);
-    val internals' = (internals1, internals2) |> Long_Name.Chunks.join
-      (K (fn ((names1, names1'), (names2, names2')) =>
-        if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
-        then raise Long_Name.Chunks.SAME
-        else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
-    val externals' = (externals1, externals2) |> Change_Table.join
-      (fn name => fn ({entry = entry1, ...}, {entry = entry2, ...}) =>
-        if #serial entry1 = #serial entry2 then raise Change_Table.SAME
-        else err_dup kind' (name, entry1) (name, entry2) Position.none);
-  in make_name_space (kind', internals', externals') end;
+    val internals' = merge_internals (internals1, internals2);
+    val internals_hidden' = merge_internals (internals_hidden1, internals_hidden2);
+    val entries' = (entries1, entries2) |> Change_Table.join (fn name => fn (entry1, entry2) =>
+      if op = (apply2 #serial (entry1, entry2)) then raise Change_Table.SAME
+      else err_dup_entry kind' (name, entry1) (name, entry2) Position.none);
+    val aliases' = Symtab.merge_list (op =) (aliases1, aliases2);
+  in make_name_space (kind', internals', internals_hidden', entries', aliases') end;
 
 
 
@@ -446,72 +505,37 @@
 val base_name = Long_Name.base_name o full_name global_naming;
 
 
-(* accesses *)
-
-local
-
-fun mandatory xs = fold_rev (fn (x, b) => b ? cons x) xs [];
-
-fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
-and mandatory_prefixes1 [] = []
-  | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
-  | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
-
-fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
-
-in
-
-fun make_accesses naming binding =
-  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 (apply2 (map Long_Name.make_chunks) accesses (* FIXME suppress_chunks *), args) end;
-
-end;
-
-
 (* hide *)
 
 fun hide fully name space =
-  space |> map_name_space (fn (kind, internals, externals) =>
+  space |> map_name_space (fn (kind, internals, internals_hidden, entries, aliases) =>
     let
       val _ = the_entry space name;
-      val (accesses, accesses') =
-        (case lookup_externals space name of
-          NONE => ([], [])
-        | SOME {accesses, accesses', ...} => (accesses, accesses'));
-      val xnames = filter (is_valid_access space name) accesses;
-      val xnames' =
-        if fully then xnames
-        else inter Long_Name.eq_chunks [Long_Name.base_chunks name] xnames;
+      val hide_names = get_aliases space name;
+      val accesses =
+        maps (make_accesses {intern = true} NONE) hide_names
+        |> not fully ? inter Long_Name.eq_chunks [Long_Name.base_chunks name];
+      val accesses' = maps (make_accesses {intern = false} NONE) hide_names;
       val internals' = internals
-        |> hide_name name
-        |> fold (del_name name) xnames'
-        |> fold (del_name_extra name) accesses';
-    in (kind, internals', externals) end);
+        |> fold (del_internals name) accesses
+        |> fold (del_internals' name) accesses';
+      val internals_hidden' = internals_hidden
+        |> add_internals name (Long_Name.make_chunks name);
+    in (kind, internals', internals_hidden', entries, aliases) end);
 
 
 (* alias *)
 
 fun alias naming binding name space =
-  space |> map_name_space (fn (kind, internals, externals) =>
+  space |> map_name_space (fn (kind, internals, internals_hidden, entries, aliases) =>
     let
       val _ = the_entry space name;
-      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} =>
-            {accesses = fold_rev (update Long_Name.eq_chunks) more_accs accesses,
-             accesses' = fold_rev (update Long_Name.eq_chunks) more_accs' accesses',
-             entry = entry});
-    in (kind, internals', externals') end);
+      val {restriction, suppress, full_name = alias_name, ...} = name_spec naming binding;
+      val _ = alias_name = "" andalso error (Binding.bad binding);
+      val alias_accesses = make_accesses {intern = true} restriction (suppress, alias_name);
+      val internals' = internals |> fold (add_internals name) alias_accesses;
+      val aliases' = aliases |> Symtab.update_list (op =) (name, (suppress, alias_name));
+    in (kind, internals', internals_hidden, entries, aliases') end);
 
 
 
@@ -540,36 +564,33 @@
 
 (* declaration *)
 
-fun declared (Name_Space {externals, ...}) = Change_Table.defined externals;
+fun declared (Name_Space {entries, ...}) = Change_Table.defined entries;
 
 fun declare context strict binding space =
   let
     val naming = naming_of context;
     val Naming {group, theory_long_name, ...} = naming;
-    val ((accesses, accesses'), {concealed, full_name = name, ...}) = make_accesses naming binding;
+    val name_spec as {restriction, suppress, full_name = name, ...} = name_spec naming binding;
     val _ = name = "" andalso error (Binding.bad binding);
+    val accesses = make_accesses {intern = true} restriction (suppress, name);
 
     val (proper_pos, pos) = Position.default (Binding.pos_of binding);
-    val entry =
-     {concealed = concealed,
+    val entry: entry =
+     {concealed = #concealed name_spec,
+      suppress = suppress,
       group = group,
       theory_long_name = theory_long_name,
       pos = pos,
       serial = serial ()};
     val space' =
-      space |> map_name_space (fn (kind, internals, externals) =>
+      space |> map_name_space (fn (kind, internals, internals_hidden, entries, aliases) =>
         let
-          val internals' = internals |> fold (add_name name) accesses;
-          val externals' =
-            (if strict then Change_Table.update_new else Change_Table.update)
-              (name, {accesses = accesses, accesses' = accesses', entry = entry}) externals
-            handle Change_Table.DUP dup =>
-              err_dup kind (dup, #entry (the (lookup_externals space dup)))
-                (name, entry) (#pos entry);
-        in (kind, internals', externals') end);
+          val internals' = internals |> fold (add_internals name) accesses;
+          val entries' = entries |> update_entry strict kind (name, entry);
+        in (kind, internals', internals_hidden, entries', aliases) end);
     val _ =
       if proper_pos andalso Context_Position.is_reported_generic context pos then
-        Position.report pos (entry_markup {def = true} (kind_of space) (name, entry))
+        Position.report pos (markup_entry {def = true} (kind_of space) (name, entry))
       else ();
   in (name, space') end;
 
@@ -596,7 +617,7 @@
             |> map (fn pos => (pos, markup space name));
         in ((name, reports), x) end
     | NONE =>
-        error (undefined space name ^ Position.here_list ps ^
+        error (undefined_entry space name ^ Position.here_list ps ^
           Completion.markup_report
             (map (fn pos => completion context space (K true) (xname, pos)) ps)))
   end;
@@ -614,7 +635,7 @@
 fun get table name =
   (case lookup_key table name of
     SOME (_, x) => x
-  | NONE => error (undefined (space_of_table table) name));
+  | NONE => error (undefined_entry (space_of_table table) name));
 
 fun define context strict (binding, x) (Table (space, tab)) =
   let

--- a/src/Pure/General/table.ML	Sun May 07 14:52:53 2023 +0100
+++ b/src/Pure/General/table.ML	Sun May 07 22:51:23 2023 +0200
@@ -56,8 +56,8 @@
   val lookup_list: 'a list table -> key -> 'a list
   val cons_list: key * 'a -> 'a list table -> 'a list table
   val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
+  val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
   val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table
-  val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
   val make_list: (key * 'a) list -> 'a list table
   val dest_list: 'a list table -> (key * 'a) list
   val merge_list: ('a * 'a -> bool) -> 'a list table * 'a list table -> 'a list table
@@ -621,20 +621,27 @@
 
 fun cons_list (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab;
 
-fun insert_list eq (key, x) =
-  modify key (fn NONE => [x] | SOME xs => if Library.member eq xs x then raise SAME else x :: xs);
+fun modify_list key f =
+  modify key (fn arg =>
+    let
+      val xs = the_default [] arg;
+      val ys = f xs;
+    in if pointer_eq (xs, ys) then raise SAME else ys end);
+
+fun insert_list eq (key, x) = modify_list key (Library.insert eq x);
+fun update_list eq (key, x) = modify_list key (Library.update eq x);
 
 fun remove_list eq (key, x) tab =
-  map_entry key (fn xs => (case Library.remove eq x xs of [] => raise UNDEF key | ys => ys)) tab
+  map_entry key (fn xs =>
+    (case Library.remove eq x xs of
+      [] => raise UNDEF key
+    | ys => if pointer_eq (xs, ys) then raise SAME else ys)) tab
   handle UNDEF _ => delete key tab;
 
-fun update_list eq (key, x) =
-  modify key (fn NONE => [x] | SOME [] => [x] | SOME (xs as y :: _) =>
-    if eq (x, y) then raise SAME else Library.update eq x xs);
-
 fun make_list args = build (fold_rev cons_list args);
 fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab);
-fun merge_list eq = join (fn _ => Library.merge eq);
+fun merge_list eq =
+  join (fn _ => fn xy => if eq_list eq xy then raise SAME else Library.merge eq xy);
 
 
 (* set operations *)

--- a/src/Pure/Isar/class_declaration.ML	Sun May 07 14:52:53 2023 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Sun May 07 22:51:23 2023 +0200
@@ -322,13 +322,13 @@
 fun gen_class prep_class_spec b raw_includes raw_supclasses raw_elems thy =
   let
     val class = Sign.full_name thy b;
-    val prefix = Binding.qualify true "class";
     val ctxt = Proof_Context.init_global thy;
     val (((sups, supparam_names), (supsort, base_sort, supexpr)), (includes, elems, global_syntax)) =
       prep_class_spec ctxt raw_supclasses raw_includes raw_elems;
+    val of_class_binding = Binding.qualify_name true b "intro_of_class";
   in
     thy
-    |> Expression.add_locale b (prefix b) includes supexpr elems
+    |> Expression.add_locale b (Binding.qualify true "class" b) includes supexpr elems
     |> snd |> Local_Theory.exit_global
     |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
     |-> (fn (param_map, params, assm_axiom) =>
@@ -339,7 +339,7 @@
            mixin = Option.map (rpair true) eq_morph,
            export = export_morph})
     #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
-    #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
+    #> Global_Theory.store_thm (of_class_binding, of_class)))
     |> snd
     |> Named_Target.init includes class
     |> pair class

--- a/src/Pure/library.ML	Sun May 07 14:52:53 2023 +0100
+++ b/src/Pure/library.ML	Sun May 07 22:51:23 2023 +0200
@@ -198,7 +198,7 @@
   val is_greater_equal: order -> bool
   val rev_order: order -> order
   val make_ord: ('a * 'a -> bool) -> 'a ord
-  val pointer_eq_ord: ('a * 'a -> order) -> 'a * 'a -> order
+  val pointer_eq_ord: 'a ord -> 'a ord
   val bool_ord: bool ord
   val int_ord: int ord
   val string_ord: string ord
@@ -371,12 +371,21 @@
 
 (* basic list functions *)
 
-fun eq_list eq (list1, list2) =
-  pointer_eq (list1, list2) orelse
-    let
-      fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys)
-        | eq_lst _ = true;
-    in length list1 = length list2 andalso eq_lst (list1, list2) end;
+fun eq_list eq lists =
+  let
+    fun eq_len args =
+      pointer_eq args orelse
+        (case args of
+          (_ :: xs, _ :: ys) => eq_len (xs, ys)
+        | ([], []) => true
+        | _ => false);
+    fun eq_lst args =
+      pointer_eq args orelse
+        (case args of
+          (x :: xs, y :: ys) => eq (x, y) andalso eq_lst (xs, ys)
+        | ([], []) => true
+        | _ => false);
+  in eq_len lists andalso eq_lst lists end;
 
 fun maps f [] = []
   | maps f (x :: xs) = f x @ maps f xs;
@@ -607,9 +616,8 @@
       else ([], (xs, ys));
 
 fun prefixes1 [] = []
-  | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
-
-fun prefixes xs = [] :: prefixes1 xs;
+  | prefixes1 (x :: xs) = map (cons x) (prefixes xs)
+and prefixes xs = [] :: prefixes1 xs;
 
 fun suffixes1 xs = map rev (prefixes1 (rev xs));
 fun suffixes xs = [] :: suffixes1 xs;
@@ -828,7 +836,13 @@
 
 fun insert eq x xs = if member eq xs x then xs else x :: xs;
 fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs;
-fun update eq x xs = cons x (remove eq x xs);
+
+fun update eq x list =
+  (case list of
+    [] => [x]
+  | y :: rest =>
+      if member eq rest x then x :: remove eq x list
+      else if eq (x, y) then list else x :: list);
 
 fun inter eq xs = filter (member eq xs);
 
@@ -955,15 +969,17 @@
   | dict_ord _ ([], _ :: _) = LESS
   | dict_ord _ (_ :: _, []) = GREATER;
 
-(*lexicographic product of lists*)
-fun length_ord (xs, ys) = int_ord (length xs, length ys);
-fun list_ord elem_ord = length_ord ||| dict_ord elem_ord;
+fun length_ord args =
+  (case args of
+    (_ :: xs, _ :: ys) => length_ord (xs, ys)
+  | ([], []) => EQUAL
+  | ([], _ :: _) => LESS
+  | (_ :: _, []) => GREATER);
 
-fun vector_ord ord =
-  pointer_eq_ord (int_ord o apply2 Vector.length ||| Vector.collate ord);
-
-fun array_ord ord =
-  pointer_eq_ord (int_ord o apply2 Array.length ||| Array.collate ord);
+(*lexicographic product of lists, vectors, arrays*)
+fun list_ord elem_ord = length_ord ||| dict_ord elem_ord;
+fun vector_ord ord = pointer_eq_ord (int_ord o apply2 Vector.length ||| Vector.collate ord);
+fun array_ord ord = pointer_eq_ord (int_ord o apply2 Array.length ||| Array.collate ord);
 
 
 (* sorting *)

--- a/src/Pure/thm.ML	Sun May 07 14:52:53 2023 +0100
+++ b/src/Pure/thm.ML	Sun May 07 22:51:23 2023 +0200
@@ -400,7 +400,6 @@
 in
 
 val union_constraints = Ord_List.union constraint_ord;
-val unions_constraints = Ord_List.unions constraint_ord;
 
 fun insert_constraints thy (T, S) =
   let
@@ -481,7 +480,6 @@
 
 
 val union_hyps = Ord_List.union Term_Ord.fast_term_ord;
-val unions_hyps = Ord_List.unions Term_Ord.fast_term_ord;
 val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord;
 val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord;
 
@@ -503,7 +501,6 @@
 
 val maxidx_of = #maxidx o rep_thm;
 fun maxidx_thm th i = Int.max (maxidx_of th, i);
-val constraints_of = #constraints o rep_thm;
 val shyps_of = #shyps o rep_thm;
 val hyps_of = #hyps o rep_thm;
 val prop_of = #prop o rep_thm;

--- a/src/Pure/variable.ML	Sun May 07 14:52:53 2023 +0100
+++ b/src/Pure/variable.ML	Sun May 07 22:51:23 2023 +0200
@@ -433,7 +433,7 @@
       ctxt
       |> map_fixes
         (Name_Space.define context true (Binding.make (x', pos), (x, proper)) #> snd #>
-          Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x')
+          x <> "" ? Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x')
       |> declare_fixed x
       |> declare_constraints (Syntax.free x')
   end;

--- a/src/Tools/Code/code_symbol.ML	Sun May 07 14:52:53 2023 +0100
+++ b/src/Tools/Code/code_symbol.ML	Sun May 07 22:51:23 2023 +0200
@@ -97,8 +97,9 @@
 end;
 
 local
-  val thyname_of_type = Name_Space.the_entry_theory_name o Sign.type_space;
-  val thyname_of_class = Name_Space.the_entry_theory_name o Sign.class_space;
+  val thyname_of = Name_Space.theory_name {long = false};
+  val thyname_of_type = thyname_of o Sign.type_space;
+  val thyname_of_class = thyname_of o Sign.class_space;
   fun thyname_of_instance thy inst = case Thm.theory_names_of_arity {long = false} thy inst
    of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^  snd inst))
     | thyname :: _ => thyname;
@@ -106,7 +107,7 @@
    of SOME class => thyname_of_class thy class
     | NONE => (case Code.get_type_of_constr_or_abstr thy c
        of SOME (tyco, _) => thyname_of_type thy tyco
-        | NONE => Name_Space.the_entry_theory_name (Sign.const_space thy) c);
+        | NONE => thyname_of (Sign.const_space thy) c);
   fun prefix thy (Constant "") = "Code"
     | prefix thy (Constant c) = thyname_of_const thy c
     | prefix thy (Type_Constructor tyco) = thyname_of_type thy tyco