src/HOL/Tools/datatype_realizer.ML
changeset 31458 b1cf26f2919b
parent 30435 e62d6ecab6ad
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Thu Jun 04 16:11:03 2009 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Thu Jun 04 16:11:04 2009 +0200
     1.3 @@ -56,17 +56,17 @@
     1.4      fun mk_all i s T t =
     1.5        if i mem is then list_all_free ([(s, T)], t) else t;
     1.6  
     1.7 -    val (prems, rec_fns) = split_list (List.concat (snd (Library.foldl_map
     1.8 -      (fn (j, ((i, (_, _, constrs)), T)) => Library.foldl_map (fn (j, (cname, cargs)) =>
     1.9 +    val (prems, rec_fns) = split_list (flat (fst (fold_map
    1.10 +      (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
    1.11          let
    1.12            val Ts = map (typ_of_dtyp descr sorts) cargs;
    1.13            val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
    1.14 -          val recs = List.filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
    1.15 +          val recs = filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
    1.16            val frees = tnames ~~ Ts;
    1.17  
    1.18            fun mk_prems vs [] = 
    1.19                  let
    1.20 -                  val rT = List.nth (rec_result_Ts, i);
    1.21 +                  val rT = nth (rec_result_Ts) i;
    1.22                    val vs' = filter_out is_unit vs;
    1.23                    val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
    1.24                    val f' = Envir.eta_contract (list_abs_free
    1.25 @@ -80,7 +80,7 @@
    1.26                    val k = body_index dt;
    1.27                    val (Us, U) = strip_type T;
    1.28                    val i = length Us;
    1.29 -                  val rT = List.nth (rec_result_Ts, k);
    1.30 +                  val rT = nth (rec_result_Ts) k;
    1.31                    val r = Free ("r" ^ s, Us ---> rT);
    1.32                    val (p, f) = mk_prems (vs @ [r]) ds
    1.33                  in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
    1.34 @@ -89,9 +89,8 @@
    1.35                        (app_bnds (Free (s, T)) i))), p)), f)
    1.36                  end
    1.37  
    1.38 -        in (j + 1,
    1.39 -          apfst (curry list_all_free frees) (mk_prems (map Free frees) recs))
    1.40 -        end) (j, constrs)) (1, descr ~~ recTs))));
    1.41 +        in (apfst (curry list_all_free frees) (mk_prems (map Free frees) recs), j + 1) end)
    1.42 +          constrs) (descr ~~ recTs) 1)));
    1.43   
    1.44      fun mk_proj j [] t = t
    1.45        | mk_proj j (i :: is) t = if null is then t else