src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 58340 5f6f48e87de6
parent 58203 9003cc8ac94d
child 58352 37745650a3f4
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Sep 15 11:54:47 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Sep 15 12:11:41 2014 +0200
     1.3 @@ -47,8 +47,8 @@
     1.4      Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
     1.5    end;
     1.6  
     1.7 -fun construct_mutualized_fp fp cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
     1.8 -    (absT_infos : absT_info list) lthy =
     1.9 +fun construct_mutualized_fp fp mutual_cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss)
    1.10 +    bnfs (absT_infos : absT_info list) lthy =
    1.11    let
    1.12      fun of_fp_res get =
    1.13        map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
    1.14 @@ -273,15 +273,15 @@
    1.15            map (typ_subst_nonatomic_sorted (map (rpair dummyT)
    1.16              (As @ sort (int_ord o pairself Term.size_of_typ) fpTs))) fold_preTs';
    1.17  
    1.18 -        val (clique, TUs) =
    1.19 +        val (mutual_clique, TUs) =
    1.20            map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
    1.21            |>> map subst
    1.22            |> `(fn (_, Ys) =>
    1.23 -            nth cliques (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs))
    1.24 +            nth mutual_cliques (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs))
    1.25            ||> uncurry (map2 mk_co_algT);
    1.26 -        val cands = cliques ~~ map2 mk_co_algT fold_preTs' Xs;
    1.27 +        val cands = mutual_cliques ~~ map2 mk_co_algT fold_preTs' Xs;
    1.28          val js = find_indices (fn ((cl, cand), TU) =>
    1.29 -          cl = clique andalso Type.could_unify (TU, cand)) TUs cands;
    1.30 +          cl = mutual_clique andalso Type.could_unify (TU, cand)) TUs cands;
    1.31          val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
    1.32        in
    1.33          force_typ names_lthy (Tpats ---> TU) raw_rec