# HG changeset patch
# User wenzelm
# Date 1667476253 -3600
# Node ID 2768a6d71570cea56c6865445d51aebad561fb81
# Parent  7e1a72af970b1cd4513158c8518c7c2cf39b1ec5
tuned;

diff -r 7e1a72af970b -r 2768a6d71570 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Nov 02 16:13:29 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Nov 03 12:50:53 2022 +0100
@@ -594,7 +594,7 @@
 
 val assign_update_empty: assign_update = Inttab.empty;
 fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id;
-fun assign_update_change entry (tab: assign_update) = Inttab.update entry tab;
+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) =