# HG changeset patch
# User wenzelm
# Date 1683320628 -7200
# Node ID 305a6902abb3c8562feca4cae09726770a12f797
# Parent  b256ac9c0577c6263aeeb5d6a70157479eb3eb0f
unused;

diff -r b256ac9c0577 -r 305a6902abb3 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri May 05 22:57:10 2023 +0200
+++ b/src/Pure/General/name_space.ML	Fri May 05 23:03:48 2023 +0200
@@ -115,8 +115,7 @@
   serial: serial};
 
 type alias =
-  {decl: string,
-   suppress: bool list,
+  {suppress: bool list,
    pos: Position.T,
    serial: serial};
 
@@ -160,12 +159,6 @@
 fun hide_name name = map_internals (apsnd (update (op =) name)) (Long_Name.make_chunks name);
 
 
-(* external accesses *)
-
-type external = {aliases: string list, entry: entry};
-type externals = external Change_Table.T;  (*name -> external*)
-
-
 (* accesses *)
 
 local
@@ -558,7 +551,6 @@
           if name <> alias_name andalso (new_entry orelse strict) then
             entries |> update_entry strict kind (alias_name,
               Alias {
-                decl = name,
                 suppress = suppress,
                 pos = #2 (Position.default (Binding.pos_of binding)),
                 serial = serial ()})