made N2M more robust w.r.t. identical nested types
authortraytel
Fri Feb 14 14:54:08 2014 +0100 (2014-02-14)
changeset 554783a6efda01da4
parent 55477 6ec4d06297a5
child 55479 ece4910c3ea0
made N2M more robust w.r.t. identical nested types
src/HOL/Tools/BNF/bnf_fp_n2m.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Feb 14 13:45:29 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Feb 14 14:54:08 2014 +0100
     1.3 @@ -195,9 +195,12 @@
     1.4          val approx_fold = un_fold_of raw_iters
     1.5            |> force_typ names_lthy
     1.6              (replicate (nth ns i) dummyT ---> (if is_rec then TU_rec else TU));
     1.7 -        val TUs = binder_fun_types (Term.typ_subst_atomic (Xs ~~ fpTs) (fastype_of approx_fold));
     1.8 -        val js = find_indices Type.could_unify
     1.9 -          TUs (map (Term.typ_subst_atomic (Xs ~~ fpTs)) fold_strTs);
    1.10 +        val subst = Term.typ_subst_atomic (Xs ~~ fpTs);
    1.11 +        val TUs = map_split dest_co_algT (binder_fun_types (fastype_of approx_fold))
    1.12 +          |>> map subst
    1.13 +          |> uncurry (map2 mk_co_algT);
    1.14 +        val js = find_indices Type.could_unify TUs
    1.15 +          (map2 (fn T => fn U => mk_co_algT (subst T) U) fold_preTs Xs);
    1.16          val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
    1.17          val iter = raw_iters |> (if is_rec then co_rec_of else un_fold_of);
    1.18        in