# HG changeset patch
# User wenzelm
# Date 1667572463 -3600
# Node ID 773844f3273d433ffbfc49dfb4500d8f1b7d87d3
# Parent  bb96846e27f8e28864045c9d0e36c5231aec56d3
tuned signature;

diff -r bb96846e27f8 -r 773844f3273d src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Nov 04 15:15:25 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Nov 04 15:34:23 2022 +0100
@@ -591,7 +591,7 @@
 fun assign_update_change entry (tab: assign_update) : assign_update = Inttab.update entry tab;
 fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node;
 
-fun assign_update_new upd (tab: assign_update) =
+fun assign_update_new upd (tab: assign_update) : assign_update =
   Inttab.update_new upd tab
     handle Inttab.DUP dup => err_dup "exec state assignment" dup;