# HG changeset patch
# User wenzelm
# Date 1683654431 -7200
# Node ID 2587b492664ad3b175f0a8de457e7fa856d6830c
# Parent  006cb47a2700ef35318f53821c5a332d88cb3050
tuned;

diff -r 006cb47a2700 -r 2587b492664a src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue May 09 19:35:46 2023 +0200
+++ b/src/Pure/Syntax/parser.ML	Tue May 09 19:47:11 2023 +0200
@@ -36,7 +36,8 @@
 fun tags_content (tags: tags) = sort_by #1 (Symtab.dest tags);
 fun tags_lookup (tags: tags) = Symtab.lookup tags;
 fun tags_insert tag (tags: tags) = Symtab.update_new tag tags;
-fun tags_name (tags: tags) = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
+fun tags_name (tags: tags) =
+  the o Inttab.lookup (Inttab.build (Symtab.fold (Inttab.update_new o swap) tags));
 
 type nts = Intset.T;
 val nts_empty: nts = Intset.empty;