diff -r e94cd4f71d0c -r f5019700efa5 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:33:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:33:15 2014 +0200
@@ -86,7 +86,8 @@
         map_sels = [],
         rel_injects = @{thms rel_sum_simps(1,4)},
         rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]},
-        rel_sels = []},
+        rel_sels = [],
+        rel_intros = []},
      fp_co_induct_sugar =
        {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
         common_co_inducts = @{thms sum.induct},
@@ -133,7 +134,8 @@
         map_sels = [],
         rel_injects = @{thms rel_prod_apply},
         rel_distincts = [],
-        rel_sels = []},
+        rel_sels = [],
+        rel_intros = []},
      fp_co_induct_sugar =
        {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
         common_co_inducts = @{thms prod.induct},