src/Pure/General/array.ML

--- a/src/Pure/General/array.ML	Thu Apr 20 21:26:35 2023 +0200
+++ b/src/Pure/General/array.ML	Thu Apr 20 23:04:04 2023 +0200
@@ -8,6 +8,7 @@
 sig
   include ARRAY
   val nth: 'a array -> int -> 'a
+  val upd: 'a array -> int -> 'a -> unit
   val forall: ('a -> bool) -> 'a array -> bool
   val member: ('a * 'a -> bool) -> 'a array -> 'a -> bool
   val fold: ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
@@ -20,6 +21,7 @@
 open Array;
 
 fun nth arr i = sub (arr, i);
+fun upd arr i x = update (arr, i, x);
 
 val forall = all;