--- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Apr 22 15:34:37 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Apr 14 20:29:42 2016 +0200
@@ -1847,7 +1847,8 @@
lthy) = lthy
|> derive_xtor_co_recs Least_FP external_bs mk_Ts (Dss, resDs) bnfs
(export ctors) (export folds)
- ctor_fold_unique_thm ctor_fold_thms ctor_fold_transfer_thms ctor_Imap_thms ctor_Irel_thms;
+ ctor_fold_unique_thm ctor_fold_thms ctor_fold_transfer_thms ctor_Imap_thms ctor_Irel_thms
+ (replicate n NONE);
val timer = time (timer "recursor");