--- 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]}, []]],