src/HOL/Tools/datatype_abs_proofs.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 17261 193b84a70ca4
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -97,7 +97,7 @@
     1.4  
     1.5      val descr' = List.concat descr;
     1.6      val recTs = get_rec_types descr' sorts;
     1.7 -    val used = Library.foldr add_typ_tfree_names (recTs, []);
     1.8 +    val used = foldr add_typ_tfree_names [] recTs;
     1.9      val newTs = Library.take (length (hd descr), recTs);
    1.10  
    1.11      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    1.12 @@ -139,7 +139,7 @@
    1.13            end;
    1.14  
    1.15          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    1.16 -        val (_, _, prems, t1s, t2s) = Library.foldr mk_prem (cargs ~~ Ts, (1, 1, [], [], []))
    1.17 +        val (_, _, prems, t1s, t2s) = foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
    1.18  
    1.19        in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop (HOLogic.mk_mem
    1.20          (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), t1s),
    1.21 @@ -269,7 +269,7 @@
    1.22  
    1.23      val descr' = List.concat descr;
    1.24      val recTs = get_rec_types descr' sorts;
    1.25 -    val used = Library.foldr add_typ_tfree_names (recTs, []);
    1.26 +    val used = foldr add_typ_tfree_names [] recTs;
    1.27      val newTs = Library.take (length (hd descr), recTs);
    1.28      val T' = TFree (variant used "'t", HOLogic.typeS);
    1.29  
    1.30 @@ -401,7 +401,7 @@
    1.31          val t = if k = 0 then HOLogic.zero else
    1.32            foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.mk_nat 1])
    1.33        in
    1.34 -        Library.foldr (fn (T, t') => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT, t)
    1.35 +        foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
    1.36        end;
    1.37  
    1.38      val fs = List.concat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr');