# HG changeset patch
# User wenzelm
# Date 1667570723 -3600
# Node ID 82bd2cfafe4c4de646ac490ddbaaeb9313dcb7d2
# Parent  98bf45a5b508a2e58e38d34c4a774ec2896d85c0
tuned;

diff -r 98bf45a5b508 -r 82bd2cfafe4c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Nov 04 14:53:25 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Nov 04 15:05:23 2022 +0100
@@ -824,7 +824,7 @@
     val nodes = nodes_of new_version;
     val required = make_required nodes;
     val required0 = make_required (nodes_of old_version);
-    val edited = Symtab.build (edits |> fold (fn (name, _) => Symtab.update (name, ())));
+    val edited = Symtab.build (edits |> fold (Symtab.insert_set o #1));
 
     val updated = timeit "Document.update" (fn () =>
       nodes |> String_Graph.schedule