diff -r b6d444194280 -r 03e134d5f867 src/Pure/Concurrent/unsynchronized.ML --- a/src/Pure/Concurrent/unsynchronized.ML Sat May 15 17:38:49 2021 +0200 +++ b/src/Pure/Concurrent/unsynchronized.ML Sat May 15 17:40:36 2021 +0200 @@ -13,6 +13,7 @@ val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b val inc: int ref -> int val dec: int ref -> int + val add: int ref -> int -> int val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c end; @@ -29,6 +30,7 @@ fun inc i = (i := ! i + (1: int); ! i); fun dec i = (i := ! i - (1: int); ! i); +fun add i n = (i := ! i + (n: int); ! i); fun setmp flag value f x = Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>