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