diff -r 15176172701e -r e85c42f4f30a src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Wed Feb 17 17:08:03 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Wed Feb 17 17:08:36 2016 +0100
@@ -90,6 +90,7 @@
         rel_sels = @{thms rel_sum_sel},
         rel_intros = @{thms rel_sum.intros},
         rel_cases = @{thms rel_sum.cases},
+        pred_injects = @{thms pred_sum_inject},
         set_thms = @{thms sum_set_simps},
         set_selssss = [[[@{thms set_sum_sel(1)}], [[]]], [[[]], [@{thms set_sum_sel(2)}]]],
         set_introssss = [[[@{thms setl.intros[OF refl]}], [[]]],
@@ -154,11 +155,12 @@
        {map_thms = @{thms map_prod_simp},
         map_disc_iffs = [],
         map_selss = [@{thms fst_map_prod snd_map_prod}],
-        rel_injects = @{thms rel_prod_apply},
+        rel_injects = @{thms rel_prod_inject},
         rel_distincts = [],
         rel_sels = @{thms rel_prod_sel},
         rel_intros = @{thms rel_prod.intros},
         rel_cases = @{thms rel_prod.cases},
+        pred_injects = @{thms pred_prod_inject},
         set_thms = @{thms prod_set_simps},
         set_selssss = [[[@{thms fsts.intros}, []]], [[[], @{thms snds.intros}]]],
         set_introssss = [[[@{thms fsts.intros[of "(a, b)" for a b, unfolded fst_conv]}, []]],