--- a/src/HOL/Tools/datatype_abs_proofs.ML Sun Mar 01 16:48:06 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Sun Mar 01 23:36:12 2009 +0100
@@ -96,7 +96,7 @@
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
- val used = foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = Library.take (length (hd descr), recTs);
val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
@@ -140,7 +140,7 @@
end;
val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val (_, _, prems, t1s, t2s) = foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
+ val (_, _, prems, t1s, t2s) = List.foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
(rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
@@ -280,7 +280,7 @@
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
- val used = foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = Library.take (length (hd descr), recTs);
val T' = TFree (Name.variant used "'t", HOLogic.typeS);