use mutual clique information (cf. c451cf8b29c8) to make N2M more robust

--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Apr 10 09:38:38 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Apr 10 10:52:48 2014 +0200
@@ -272,12 +272,15 @@
         val fold_pre_deads_only_Ts =
           map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ fpTs))) fold_preTs';
 
-        val TUs = map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
+        val (clique, TUs) =
+          map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
           |>> map subst
-          |> uncurry (map2 mk_co_algT);
-        val cands = map2 mk_co_algT fold_preTs' Xs;
-
-        val js = find_indices Type.could_unify TUs cands;
+          |> `(fn (_, Ys) =>
+            nth cliques (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs))
+          ||> uncurry (map2 mk_co_algT);
+        val cands = cliques ~~ map2 mk_co_algT fold_preTs' Xs;
+        val js = find_indices (fn ((cl, cand), TU) =>
+          cl = clique andalso Type.could_unify (TU, cand)) TUs cands;
         val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
       in
         force_typ names_lthy (Tpats ---> TU) raw_rec