# HG changeset patch
# User blanchet
# Date 1425397065 -3600
# Node ID 913c4afb03887a77ed69753aef8791591d0d4a0b
# Parent  55f5e1cbf2a756b651bf814e48be2a490dd7040f
avoid duplicate simp warning for datatypes with explicit products

diff -r 55f5e1cbf2a7 -r 913c4afb0388 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 03 16:37:45 2015 +0100
@@ -59,7 +59,7 @@
 fun mk_unabs_def_unused_0 n =
   funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong);
 
-val size_gen_o_map_simps = @{thms prod.inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
+val size_gen_o_map_simps = @{thms inj_on_id snd_comp_apfst[unfolded apfst_def]};
 
 fun mk_size_gen_o_map_tac ctxt size_def rec_o_map inj_maps size_maps =
   unfold_thms_tac ctxt [size_def] THEN
@@ -236,7 +236,8 @@
          |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm)));
 
       val nested_size_maps = map (mk_pointfull lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps;
-      val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs)
+      val all_inj_maps =
+        @{thm prod.inj_map} :: map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs)
         |> distinct Thm.eq_thm_prop;
 
       fun derive_size_simp size_def' simp0 =