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