# HG changeset patch
# User desharna
# Date 1415705436 -3600
# Node ID 6b6032e99a4bb4981ca8350b475bca9206b74e07
# Parent  0297e1277ed2ab87375a638835c4829948b257be
also generate '(co)rec_transfer' for (co)datatypes with 0 live type variables

diff -r 0297e1277ed2 -r 6b6032e99a4b src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Nov 11 10:26:08 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Nov 11 12:30:36 2014 +0100
@@ -2318,8 +2318,7 @@
             type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
 
         val rec_transfer_thmss =
-          if live = 0 then replicate nn []
-          else map single (derive_rec_transfer_thms lthy recs rec_defs recs_args_types);
+          map single (derive_rec_transfer_thms lthy recs rec_defs recs_args_types);
 
         val induct_type_attr = Attrib.internal o K o Induct.induct_type;
         val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
@@ -2487,9 +2486,7 @@
 
         val flat_corec_thms = append oo append;
 
-        val corec_transfer_thmss =
-          if live = 0 then replicate nn []
-          else map single (derive_corec_transfer_thms lthy corecs corec_defs);
+        val corec_transfer_thmss = map single (derive_corec_transfer_thms lthy corecs corec_defs);
 
         val ((rel_coinduct_thmss, common_rel_coinduct_thms),
              (rel_coinduct_attrs, common_rel_coinduct_attrs)) =