src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 56487 961b34963fa4
parent 56486 753b779d070d
child 56638 092a306bcc3d
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Apr 10 09:38:38 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Apr 10 10:52:48 2014 +0200
     1.3 @@ -272,12 +272,15 @@
     1.4          val fold_pre_deads_only_Ts =
     1.5            map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ fpTs))) fold_preTs';
     1.6  
     1.7 -        val TUs = map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
     1.8 +        val (clique, TUs) =
     1.9 +          map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
    1.10            |>> map subst
    1.11 -          |> uncurry (map2 mk_co_algT);
    1.12 -        val cands = map2 mk_co_algT fold_preTs' Xs;
    1.13 -
    1.14 -        val js = find_indices Type.could_unify TUs cands;
    1.15 +          |> `(fn (_, Ys) =>
    1.16 +            nth cliques (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs))
    1.17 +          ||> uncurry (map2 mk_co_algT);
    1.18 +        val cands = cliques ~~ map2 mk_co_algT fold_preTs' Xs;
    1.19 +        val js = find_indices (fn ((cl, cand), TU) =>
    1.20 +          cl = clique andalso Type.could_unify (TU, cand)) TUs cands;
    1.21          val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
    1.22        in
    1.23          force_typ names_lthy (Tpats ---> TU) raw_rec