1.1 --- a/src/HOL/Tools/refute.ML	Fri Jan 05 14:32:07 2007 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Jan 05 15:33:05 2007 +0100
     1.3 @@ -2229,7 +2229,21 @@
     1.4  												result
     1.5  											end
     1.6  									(* compute all entries in INTRS for the current datatype (given by 'index') *)
     1.7 -									val _ = Array.modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((Option.valOf o AList.lookup (op =) INTRS) index)
     1.8 +									(* TODO: we can use Array.modify instead once PolyML conforms to the ML standard *)
     1.9 +									(* (int * 'a -> 'a) -> 'a array -> unit *)
    1.10 +									fun modifyi f arr =
    1.11 +										let
    1.12 +											val size = Array.length arr
    1.13 +											fun modifyi_loop i =
    1.14 +												if i < size then (
    1.15 +													Array.update (arr, i, f (i, Array.sub (arr, i)));
    1.16 +													modifyi_loop (i+1)
    1.17 +												) else
    1.18 +													()
    1.19 +										in
    1.20 +											modifyi_loop 0
    1.21 +										end
    1.22 +									val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((Option.valOf o AList.lookup (op =) INTRS) index)
    1.23  									(* 'a Array.array -> 'a list *)
    1.24  									fun toList arr =
    1.25  										Array.foldr op:: [] arr