# HG changeset patch
# User wenzelm
# Date 1681199686 -7200
# Node ID c3330a54b9e59449619691b86eabec88c8c3198f
# Parent  53c5ad1a7ac06377660d1477a68eb5c14ffb5799
unused (see 34dd96a06c45);

diff -r 53c5ad1a7ac0 -r c3330a54b9e5 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Apr 11 09:49:30 2023 +0200
+++ b/src/Pure/General/name_space.ML	Tue Apr 11 09:54:46 2023 +0200
@@ -113,7 +113,7 @@
   pos: Position.T,
   serial: serial};
 
-fun entry_markup def kind (name, {pos, theory_long_name, serial, ...}: entry) =
+fun entry_markup def kind (name, {pos, serial, ...}: entry) =
   Position.make_entity_markup def serial kind (name, pos);
 
 fun print_entry_ref kind (name, entry) =