# HG changeset patch
# User webertj
# Date 1114016225 -7200
# Node ID 82e40c9a0f3f10e238d95680020c2595cdb1f531
# Parent  a1863ea9052b525fb48ad9d4c132e19917d0a61c
call to Array.modifyi replaced

diff -r a1863ea9052b -r 82e40c9a0f3f src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Wed Apr 20 18:01:50 2005 +0200
+++ b/src/HOL/Tools/refute.ML	Wed Apr 20 18:57:05 2005 +0200
@@ -1947,7 +1947,8 @@
 										end) descr
 									(* the recursion operator is a function that maps every element of *)
 									(* the inductive datatype (and of mutually recursive types) to an  *)
-									(* element of some result type                                     *)
+									(* element of some result type; an array entry of NONE means that  *)
+									(* the actual result has not been computed yet                     *)
 									(* (int * interpretation option Array.array) list *)
 									val INTRS = map (fn (idx, _) =>
 										let
@@ -2043,7 +2044,21 @@
 												result
 											end
 									(* compute all entries in INTRS for the current datatype (given by 'index') *)
-									val _ = Array.modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((valOf o assoc) (INTRS, index), 0, NONE)
+									(* TODO: we can use Array.modify instead once PolyML conforms to the ML standard *)
+									(* (int * 'a -> 'a) -> 'a array -> unit *)
+									fun modifyi f arr =
+										let
+											val size = Array.length arr
+											fun modifyi_loop i =
+												if i < size then (
+													Array.update (arr, i, f (i, Array.sub (arr, i)));
+													modifyi_loop (i+1)
+												) else
+													()
+										in
+											modifyi_loop 0
+										end
+									val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((valOf o assoc) (INTRS, index))
 									(* 'a Array.array -> 'a list *)
 									fun toList arr =
 										Array.foldr op:: [] arr