--- 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 ()})