src/HOL/Tools/Transfer/transfer_bnf.ML

       @ map type_name_of_bnf (#bnfs (#fp_res fp_sugar)))
     val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types
     val live = live_of_bnf (bnf_of_fp_sugar fp_sugar)
     val old_lthy = lthy
     val old_As = snd (dest_Type (#T fp_sugar))
+    val liveness =
+      BNF_FP_Def_Sugar.liveness_of_fp_bnf (length old_As) (hd (#bnfs (#fp_res fp_sugar)));
     val (unsorted_As, lthy) = mk_TFrees live lthy
     val As = map2 (Ctr_Sugar_Util.resort_tfree o snd o Ctr_Sugar_Util.dest_TFree_or_TVar)
-      old_As unsorted_As
+      (map_filter (uncurry (fn true => SOME | false => K NONE)) (liveness ~~ old_As)) unsorted_As
     val predTs = map mk_pred1T As
     val (preds, lthy) = mk_Frees "P" predTs lthy
     val args = map mk_eq_onp preds
     val cTs = map (SOME o certifyT lthy) (maps (replicate 2) As)
     val cts = map (SOME o certify lthy) args