# HG changeset patch
# User webertj
# Date 1167929548 -3600
# Node ID aa2764dda077f47c63eac69f7c229404b286ab9e
# Parent  6e3a0b25cda57aa31b82c718e0d2dd1fade93b04
using Array.modifyi (no functional change)

diff -r 6e3a0b25cda5 -r aa2764dda077 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu Jan 04 17:49:43 2007 +0100
+++ b/src/HOL/Tools/refute.ML	Thu Jan 04 17:52:28 2007 +0100
@@ -2229,21 +2229,7 @@
 												result
 											end
 									(* compute all entries in INTRS for the current datatype (given by '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)
+									val _ = Array.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