# HG changeset patch
# User webertj
# Date 1168007585 -3600
# Node ID adf64b316f070df71726837dcfacfcb396c34be2
# Parent  487b79b95a20a00d1e59f325429c1cf50e89da4e
reverted to v1.60 (PolyML 4.1.3 still has the wrong signature for Array.modifyi)

diff -r 487b79b95a20 -r adf64b316f07 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Jan 05 14:32:07 2007 +0100
+++ b/src/HOL/Tools/refute.ML	Fri Jan 05 15:33:05 2007 +0100
@@ -2229,7 +2229,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)) ((Option.valOf o AList.lookup (op =) INTRS) index)
+									(* 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)) ((Option.valOf o AList.lookup (op =) INTRS) index)
 									(* 'a Array.array -> 'a list *)
 									fun toList arr =
 										Array.foldr op:: [] arr