diff -r 8ed9fcc004fe -r a167d50eadbb src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Mon Apr 18 17:20:49 2005 +0200
+++ b/src/HOL/Tools/refute.ML	Tue Apr 19 00:14:27 2005 +0200
@@ -1945,9 +1945,6 @@
 												(#1 o interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True})
 													(Const (cname, map (typ_of_dtyp descr typ_assoc) cargs ---> c_return_typ))) cs)
 										end) descr
-									val _ = writeln (makestring index)
-									val _ = writeln (makestring descr)
-									val _ = writeln (makestring mc_intrs)
 									(* 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                                     *)
@@ -2046,22 +2043,10 @@
 												result
 											end
 									(* compute all entries in INTRS for the current datatype (given by 'index') *)
-									val size = (Array.length o valOf o assoc) (INTRS, index)
-									(* int -> unit *)
-									fun compute_loop elem =
-										if elem=size then
-											(* terminate *)
-											()
-										else (  (* elem < size *)
-											compute_array_entry index elem;
-											compute_loop (elem+1)
-										)
-									val _ = compute_loop 0
-									val _ = Array.modifyi ... ((valOf o assoc) (INTRS, index))
+									val _ = Array.modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((valOf o assoc) (INTRS, index), 0, NONE)
 									(* 'a Array.array -> 'a list *)
 									fun toList arr =
 										Array.foldr op:: [] arr
-									val _ = writeln (makestring INTRS)
 								in
 									(* return the part of 'INTRS' that corresponds to the current datatype *)
 									SOME ((Node o (map valOf) o toList o valOf o assoc) (INTRS, index), model', args')