--- 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