# HG changeset patch
# User blanchet
# Date 1407263112 -7200
# Node ID 018dc778cbcc310bbd4a3cf3739b6fa765ad5a81
# Parent  7d319d6ccde09541845aa65587b0a1e94a0dceda
more correct clique computation for N2M

diff -r 7d319d6ccde0 -r 018dc778cbcc src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Aug 05 15:55:39 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Aug 05 20:25:12 2014 +0200
@@ -80,10 +80,27 @@
     val (orig_descr' :: nested_descrs, _) =
       Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp;
 
+    fun cliquify_descr [] = []
+      | cliquify_descr [entry] = [[entry]]
+      | cliquify_descr (full_descr as (_, (T_name1, _, _)) :: _) =
+        let
+          val nn =
+            if member (op =) fpT_names T_name1 then
+              nn_fp
+            else
+              (case Symtab.lookup all_infos T_name1 of
+                SOME {descr, ...} =>
+                length (filter_out (fn (_, (_, Us, _)) => exists Datatype_Aux.is_rec_type Us) descr)
+              | NONE => raise Fail "unknown old-style datatype");
+        in
+          chop nn full_descr ||> cliquify_descr |> op ::
+        end;
+
     (* put nested types before the types that nest them, as needed for N2M *)
     val descrs = burrow reindex_desc (orig_descr' :: rev nested_descrs);
     val (cliques, descr) =
-      split_list (flat (map_index (fn (i, descr) => map (pair i) descr) descrs));
+      split_list (flat (map_index (fn (i, descr) => map (pair i) descr)
+        (maps cliquify_descr descrs)));
 
     val dest_dtyp = Datatype_Aux.typ_of_dtyp descr;