also generate '(co)rec_transfer' for (co)datatypes with 0 live type variables
authordesharna
Tue, 11 Nov 2014 12:30:36 +0100
changeset 58967 6b6032e99a4b
parent 58966 0297e1277ed2
child 58968 d09bbd2642e2
also generate '(co)rec_transfer' for (co)datatypes with 0 live type variables
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)) =