tuned;

--- a/src/HOL/Tools/sat.ML	Wed Apr 19 23:27:33 2023 +0200
+++ b/src/HOL/Tools/sat.ML	Wed Apr 19 23:27:55 2023 +0200
@@ -216,7 +216,7 @@
       handle TERM _ => NONE;  (* 'chyp' is not a literal *)
 
     fun prove_clause id =
-      (case Array.sub (clauses, id) of
+      (case Array.nth clauses id of
         RAW_CLAUSE clause => clause
       | ORIG_CLAUSE thm =>
           (* convert the original clause *)

--- a/src/HOL/Tools/sat_solver.ML	Wed Apr 19 23:27:33 2023 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Wed Apr 19 23:27:55 2023 +0200
@@ -682,7 +682,7 @@
             original_clause_id_from 0
           (* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
           (* testing for equality should suffice -- barring duplicate literals     *)
-          else if Array.sub (clauses, index) = lits then (
+          else if Array.nth clauses index = lits then (
             (* success *)
             last_ref_clause := index;
             SOME index

--- a/src/Pure/General/sha1.ML	Wed Apr 19 23:27:33 2023 +0200
+++ b/src/Pure/General/sha1.ML	Wed Apr 19 23:27:55 2023 +0200
@@ -101,12 +101,12 @@
     (*hash result -- 5 words*)
     val hash_array : Word32.word Array.array =
       Array.fromList [0wx67452301, 0wxEFCDAB89, 0wx98BADCFE, 0wx10325476, 0wxC3D2E1F0];
-    fun hash i = Array.sub (hash_array, i);
+    val hash = Array.nth hash_array;
     fun add_hash x i = Array.update (hash_array, i, hash i + x);
 
     (*current chunk -- 80 words*)
     val chunk_array = Array.array (80, 0w0: Word32.word);
-    fun chunk i = Array.sub (chunk_array, i);
+    val chunk = Array.nth chunk_array;
     fun init_chunk pos =
       Array.modifyi (fn (i, _) =>
         if i < 16 then text (pos + i)

--- a/src/Pure/Syntax/parser.ML	Wed Apr 19 23:27:33 2023 +0200
+++ b/src/Pure/Syntax/parser.ML	Wed Apr 19 23:27:55 2023 +0200
@@ -132,12 +132,12 @@
       if not new_chain then ([], lambdas)
       else
         let (*lookahead of chain's source*)
-          val ((_, from_tks), _) = Array.sub (prods, the chain);
+          val ((_, from_tks), _) = Array.nth prods (the chain);
 
           (*copy from's lookahead to chain's destinations*)
           fun copy_lookahead to =
             let
-              val ((to_nts, to_tks), ps) = Array.sub (prods, to);
+              val ((to_nts, to_tks), ps) = Array.nth prods to;
 
               val new_tks = Tokens.subtract to_tks from_tks;  (*added lookahead tokens*)
               val to_tks' = Tokens.merge (to_tks, new_tks);
@@ -170,7 +170,7 @@
           else (NONE, nts_insert nt nts);
 
     (*get all known starting tokens for a nonterminal*)
-    fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
+    fun starts_for_nt nt = snd (fst (Array.nth prods nt));
 
     (*update prods, lookaheads, and lambdas according to new lambda NTs*)
     val (added_starts', lambdas') =
@@ -180,7 +180,7 @@
           | propagate_lambda (l :: ls) added_starts lambdas =
               let
                 (*get lookahead for lambda NT*)
-                val ((dependent, l_starts), _) = Array.sub (prods, l);
+                val ((dependent, l_starts), _) = Array.nth prods l;
 
                 (*check productions whose lookahead may depend on lambda NT*)
                 fun examine_prods [] add_lambda nt_dependencies added_tks nt_prods =
@@ -221,7 +221,7 @@
                 (*check each NT whose lookahead depends on new lambda NT*)
                 fun process_nts nt (added_lambdas, added_starts) =
                   let
-                    val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
+                    val ((old_nts, old_tks), nt_prods) = Array.nth prods nt;
 
                     (*existing productions whose lookahead may depend on l*)
                     val tk_prods = prods_lookup nt_prods (get_start l_starts);
@@ -279,7 +279,7 @@
           (*add lhs NT to list of dependent NTs in lookahead*)
           fun add_nts nt initial =
             (if initial then
-              let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in
+              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))
               end
@@ -290,7 +290,7 @@
           fun add_tks [] added = added
             | add_tks (nt :: nts) added =
                 let
-                  val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
+                  val ((old_nts, old_tks), nt_prods) = Array.nth prods nt;
 
                   val new_tks = Tokens.subtract old_tks start_tks;
 
@@ -365,7 +365,7 @@
                 (*copy existing productions for new starting tokens*)
                 fun process_nts nt =
                   let
-                    val ((nts, tks), nt_prods) = Array.sub (prods, nt);
+                    val ((nts, tks), nt_prods) = Array.nth prods nt;
 
                     val tk_prods = prods_lookup nt_prods key;
 
@@ -382,7 +382,7 @@
                     val _ = Array.update (prods, nt, ((nts, tks'), nt_prods''));
                   in tokens_add (nt, added_tks) end;
 
-                val ((dependent, _), _) = Array.sub (prods, changed_nt);
+                val ((dependent, _), _) = Array.nth prods changed_nt;
               in add_starts (starts @ nts_fold process_nts dependent []) end;
       in add_starts added_starts' end;
   in (chains', lambdas') end;
@@ -574,7 +574,7 @@
   filter
     (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec
       | _ => false)
-    (Array.sub (Estate, j));
+    (Array.nth Estate j);
 
 
 fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) =
@@ -652,7 +652,7 @@
 
 
 fun produce gram stateset i indata prev_token =
-  (case Array.sub (stateset, i) of
+  (case Array.nth stateset i of
     [] =>
       let
         val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata;