# HG changeset patch
# User blanchet
# Date 1410185350 -7200
# Node ID 61e4c96bf2b6c4d95faec59b1617c58edfc3f768
# Parent  cece11f6262a1ac373280130f08ce0492fbbee33
made code work also in the presence of deads

diff -r cece11f6262a -r 61e4c96bf2b6 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 08 15:54:33 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 08 16:09:10 2014 +0200
@@ -50,6 +50,7 @@
 
   val flat_corec_preds_predsss_gettersss: 'a list -> 'a list list list -> 'a list list list ->
     'a list
+  val liveness_of_fp_bnf: int -> BNF_Def.bnf -> bool list
   val nesting_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
 
   type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list)
diff -r cece11f6262a -r 61e4c96bf2b6 src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Sep 08 15:54:33 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Sep 08 16:09:10 2014 +0200
@@ -311,9 +311,11 @@
     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