src/Pure/Concurrent/unsynchronized.ML
changeset 73696 03e134d5f867
parent 62935 3c7a35c12e03
child 77996 afa6117bace4
--- 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 () =>