src/HOL/Tools/datatype_rep_proofs.ML
changeset 30190 479806475f3c
parent 29579 cb520b766e00
child 30280 eb98b49ef835
child 30305 720226bedc4d
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sun Mar 01 16:48:06 2009 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sun Mar 01 23:36:12 2009 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4      val branchT = if null branchTs then HOLogic.unitT
     1.5        else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
     1.6      val arities = get_arities descr' \ 0;
     1.7 -    val unneeded_vars = hd tyvars \\ foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
     1.8 +    val unneeded_vars = hd tyvars \\ List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
     1.9      val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
    1.10      val recTs = get_rec_types descr' sorts;
    1.11      val newTs = Library.take (length (hd descr), recTs);
    1.12 @@ -143,7 +143,7 @@
    1.13        in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
    1.14        end;
    1.15  
    1.16 -    val mk_lim = foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
    1.17 +    val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
    1.18  
    1.19      (************** generate introduction rules for representing set **********)
    1.20  
    1.21 @@ -169,7 +169,7 @@
    1.22                in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
    1.23                end);
    1.24  
    1.25 -        val (_, prems, ts) = foldr mk_prem (1, [], []) cargs;
    1.26 +        val (_, prems, ts) = List.foldr mk_prem (1, [], []) cargs;
    1.27          val concl = HOLogic.mk_Trueprop
    1.28            (Free (s, UnivT') $ mk_univ_inj ts n i)
    1.29        in Logic.list_implies (prems, concl)
    1.30 @@ -229,7 +229,7 @@
    1.31              | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
    1.32            end;
    1.33  
    1.34 -        val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs;
    1.35 +        val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
    1.36          val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
    1.37          val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
    1.38          val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
    1.39 @@ -357,7 +357,7 @@
    1.40  
    1.41        in (thy', char_thms' @ char_thms) end;
    1.42  
    1.43 -    val (thy5, iso_char_thms) = apfst Theory.checkpoint (foldr make_iso_defs
    1.44 +    val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs
    1.45        (add_path flat_names big_name thy4, []) (tl descr));
    1.46  
    1.47      (* prove isomorphism properties *)
    1.48 @@ -447,7 +447,7 @@
    1.49        in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
    1.50        end;
    1.51  
    1.52 -    val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms
    1.53 +    val (iso_inj_thms_unfolded, iso_elem_thms) = List.foldr prove_iso_thms
    1.54        ([], map #3 newT_iso_axms) (tl descr);
    1.55      val iso_inj_thms = map snd newT_iso_inj_thms @
    1.56        map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;