diff -r d78b00f98de8 -r 2e0cf67fa89f src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:34:49 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:35:03 2014 +0200
@@ -103,6 +103,7 @@
         co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]},
         co_rec_thms = @{thms sum.case},
         co_rec_discs = [],
+        co_rec_disc_iffs = [],
         co_rec_selss = []}}
   end;
 
@@ -159,6 +160,7 @@
         co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
         co_rec_thms = @{thms prod.case},
         co_rec_discs = [],
+        co_rec_disc_iffs = [],
         co_rec_selss = []}}
   end;