--- a/src/HOL/Library/refute.ML Thu Apr 20 21:26:35 2023 +0200
+++ b/src/HOL/Library/refute.ML Thu Apr 20 23:04:04 2023 +0200
@@ -2375,7 +2375,7 @@
val result = fold (fn arg_i => fn i =>
interpretation_apply (i, arg_i)) arg_intrs intr
(* update 'REC_OPERATORS' *)
- val _ = Array.update (arr, elem, (true, result))
+ val _ = Array.upd arr elem (true, result)
in
result
end
--- a/src/HOL/Tools/sat.ML Thu Apr 20 21:26:35 2023 +0200
+++ b/src/HOL/Tools/sat.ML Thu Apr 20 23:04:04 2023 +0200
@@ -226,7 +226,7 @@
val hyps = sort (lit_ord o apply2 fst) (map_filter (fn chyp =>
Option.map (rpair chyp) (index_of_literal chyp)) (Thm.chyps_of raw))
val clause = (raw, hyps)
- val _ = Array.update (clauses, id, RAW_CLAUSE clause)
+ val _ = Array.upd clauses id (RAW_CLAUSE clause)
in
clause
end
@@ -236,7 +236,7 @@
val _ = cond_tracing ctxt (fn () => "Proving clause #" ^ string_of_int id ^ " ...")
val ids = the (Inttab.lookup clause_table id)
val clause = resolve_raw_clauses ctxt (map prove_clause ids)
- val _ = Array.update (clauses, id, RAW_CLAUSE clause)
+ val _ = Array.upd clauses id (RAW_CLAUSE clause)
val _ =
cond_tracing ctxt
(fn () => "Replay chain successful; clause stored at #" ^ string_of_int id)
@@ -358,7 +358,7 @@
val max_idx = fst (the (Inttab.max clause_table))
val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
val _ =
- fold (fn thm => fn i => (Array.update (clause_arr, i, ORIG_CLAUSE thm); i + 1))
+ fold (fn thm => fn i => (Array.upd clause_arr i (ORIG_CLAUSE thm); i + 1))
cnf_clauses 0
(* replay the proof to derive the empty clause *)
(* [c_1 && ... && c_n] |- False *)
--- a/src/HOL/Tools/sat_solver.ML Thu Apr 20 21:26:35 2023 +0200
+++ b/src/HOL/Tools/sat_solver.ML Thu Apr 20 23:04:04 2023 +0200
@@ -667,7 +667,7 @@
fun init_array (Prop_Logic.And (fm1, fm2), n) =
init_array (fm2, init_array (fm1, n))
| init_array (fm, n) =
- (Array.update (clauses, n, clause_to_lit_list fm); n+1)
+ (Array.upd clauses n (clause_to_lit_list fm); n+1)
val _ = init_array (cnf, 0)
(* optimization for the common case where MiniSat "R"s clauses in their *)
(* original order: *)
--- 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;
--- a/src/Pure/General/sha1.ML Thu Apr 20 21:26:35 2023 +0200
+++ b/src/Pure/General/sha1.ML Thu Apr 20 23:04:04 2023 +0200
@@ -102,7 +102,7 @@
val hash_array : Word32.word Array.array =
Array.fromList [0wx67452301, 0wxEFCDAB89, 0wx98BADCFE, 0wx10325476, 0wxC3D2E1F0];
val hash = Array.nth hash_array;
- fun add_hash x i = Array.update (hash_array, i, hash i + x);
+ fun add_hash x i = Array.upd hash_array i (hash i + x);
(*current chunk -- 80 words*)
val chunk_array = Array.array (80, 0w0: Word32.word);
--- a/src/Pure/Syntax/parser.ML Thu Apr 20 21:26:35 2023 +0200
+++ b/src/Pure/Syntax/parser.ML Thu Apr 20 23:04:04 2023 +0200
@@ -141,7 +141,7 @@
val new_tks = Tokens.subtract to_tks from_tks; (*added lookahead tokens*)
val to_tks' = Tokens.merge (to_tks, new_tks);
- val _ = Array.update (prods, to, ((to_nts, to_tks'), ps));
+ val _ = Array.upd prods to ((to_nts, to_tks'), ps);
in tokens_add (to, new_tks) end;
val tos = chains_all_succs chains' [lhs];
@@ -235,7 +235,7 @@
val new_tks = Tokens.merge (old_tks, added_tks);
val added_lambdas' = added_lambdas |> add_lambda ? cons nt;
- val _ = Array.update (prods, nt, ((new_nts, new_tks), nt_prods'));
+ val _ = Array.upd prods nt ((new_nts, new_tks), nt_prods');
(*N.B. that because the tks component
is used to access existing
productions we have to add new
@@ -281,7 +281,7 @@
(if initial then
let val ((old_nts, old_tks), ps) = Array.nth prods nt in
if nts_member old_nts lhs then ()
- else Array.update (prods, nt, ((nts_insert lhs old_nts, old_tks), ps))
+ else Array.upd prods nt ((nts_insert lhs old_nts, old_tks), ps)
end
else (); false);
@@ -306,9 +306,7 @@
|> nt = lhs ? Tokens.fold store start_tks';
val _ =
if not changed andalso Tokens.is_empty new_tks then ()
- else
- Array.update
- (prods, nt, ((old_nts, Tokens.merge (old_tks, new_tks)), nt_prods'));
+ else Array.upd prods nt ((old_nts, Tokens.merge (old_tks, new_tks)), nt_prods');
in add_tks nts (tokens_add (nt, new_tks) added) end;
val _ = nts_fold add_nts start_nts true;
in add_tks (chains_all_succs chains' [lhs]) [] end;
@@ -379,7 +377,7 @@
val added_tks = Tokens.subtract tks new_tks;
val tks' = Tokens.merge (tks, added_tks);
- val _ = Array.update (prods, nt, ((nts, tks'), nt_prods''));
+ val _ = Array.upd prods nt ((nts, tks'), nt_prods'');
in tokens_add (nt, added_tks) end;
val ((dependent, _), _) = Array.nth prods changed_nt;
@@ -677,8 +675,8 @@
| c :: cs =>
let
val (si, sii) = PROCESSS gram stateset i c s;
- val _ = Array.update (stateset, i, si);
- val _ = Array.update (stateset, i + 1, sii);
+ val _ = Array.upd stateset i si;
+ val _ = Array.upd stateset (i + 1) sii;
in produce gram stateset (i + 1) cs c end));
@@ -693,7 +691,7 @@
val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)];
val s = length indata + 1;
val Estate = Array.array (s, []);
- val _ = Array.update (Estate, 0, S0);
+ val _ = Array.upd Estate 0 S0;
in
get_trees (produce gram Estate 0 indata Lexicon.eof)
end;