--- a/src/ZF/ind_syntax.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/src/ZF/ind_syntax.ML Thu Mar 03 12:43:01 2005 +0100
@@ -111,7 +111,7 @@
fun union_params (rec_tm, cs) =
let val (_,args) = strip_comb rec_tm
fun is_ind arg = (type_of arg = iT)
- in case filter is_ind (args @ cs) of
+ in case List.filter is_ind (args @ cs) of
[] => empty
| u_args => fold_bal mk_Un u_args
end;
@@ -134,8 +134,8 @@
foldl_aterms (fn (cs, Const c) => Const c ins cs | (cs, _) => cs);
fun fourth (_, name, args, prems) = prems
fun add_consts_in_cts cts =
- foldl (foldl add_term_consts_2) ([], map fourth (flat cts));
- val cs = filter is_OK (add_consts_in_cts con_ty_lists)
+ Library.foldl (Library.foldl add_term_consts_2) ([], map fourth (List.concat cts));
+ val cs = List.filter is_OK (add_consts_in_cts con_ty_lists)
in u $ union_params (hd rec_tms, cs) end;