# HG changeset patch
# User traytel
# Date 1392386048 -3600
# Node ID 3a6efda01da476f0cde122a2deab2e54defedaf7
# Parent  6ec4d06297a5e11dbe8ce75ff893aad90ccab4fa
made N2M more robust w.r.t. identical nested types

diff -r 6ec4d06297a5 -r 3a6efda01da4 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Feb 14 13:45:29 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Feb 14 14:54:08 2014 +0100
@@ -195,9 +195,12 @@
         val approx_fold = un_fold_of raw_iters
           |> force_typ names_lthy
             (replicate (nth ns i) dummyT ---> (if is_rec then TU_rec else TU));
-        val TUs = binder_fun_types (Term.typ_subst_atomic (Xs ~~ fpTs) (fastype_of approx_fold));
-        val js = find_indices Type.could_unify
-          TUs (map (Term.typ_subst_atomic (Xs ~~ fpTs)) fold_strTs);
+        val subst = Term.typ_subst_atomic (Xs ~~ fpTs);
+        val TUs = map_split dest_co_algT (binder_fun_types (fastype_of approx_fold))
+          |>> map subst
+          |> uncurry (map2 mk_co_algT);
+        val js = find_indices Type.could_unify TUs
+          (map2 (fn T => fn U => mk_co_algT (subst T) U) fold_preTs Xs);
         val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
         val iter = raw_iters |> (if is_rec then co_rec_of else un_fold_of);
       in