--- 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;