--- 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)
--- 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