compilation error fixed
authorwebertj
Tue Apr 19 00:14:27 2005 +0200 (2005-04-19)
changeset 15768a167d50eadbb
parent 15767 8ed9fcc004fe
child 15769 38c8ea8521e7
compilation error fixed
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Mon Apr 18 17:20:49 2005 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Tue Apr 19 00:14:27 2005 +0200
     1.3 @@ -1945,9 +1945,6 @@
     1.4  												(#1 o interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True})
     1.5  													(Const (cname, map (typ_of_dtyp descr typ_assoc) cargs ---> c_return_typ))) cs)
     1.6  										end) descr
     1.7 -									val _ = writeln (makestring index)
     1.8 -									val _ = writeln (makestring descr)
     1.9 -									val _ = writeln (makestring mc_intrs)
    1.10  									(* the recursion operator is a function that maps every element of *)
    1.11  									(* the inductive datatype (and of mutually recursive types) to an  *)
    1.12  									(* element of some result type                                     *)
    1.13 @@ -2046,22 +2043,10 @@
    1.14  												result
    1.15  											end
    1.16  									(* compute all entries in INTRS for the current datatype (given by 'index') *)
    1.17 -									val size = (Array.length o valOf o assoc) (INTRS, index)
    1.18 -									(* int -> unit *)
    1.19 -									fun compute_loop elem =
    1.20 -										if elem=size then
    1.21 -											(* terminate *)
    1.22 -											()
    1.23 -										else (  (* elem < size *)
    1.24 -											compute_array_entry index elem;
    1.25 -											compute_loop (elem+1)
    1.26 -										)
    1.27 -									val _ = compute_loop 0
    1.28 -									val _ = Array.modifyi ... ((valOf o assoc) (INTRS, index))
    1.29 +									val _ = Array.modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((valOf o assoc) (INTRS, index), 0, NONE)
    1.30  									(* 'a Array.array -> 'a list *)
    1.31  									fun toList arr =
    1.32  										Array.foldr op:: [] arr
    1.33 -									val _ = writeln (makestring INTRS)
    1.34  								in
    1.35  									(* return the part of 'INTRS' that corresponds to the current datatype *)
    1.36  									SOME ((Node o (map valOf) o toList o valOf o assoc) (INTRS, index), model', args')