# HG changeset patch
# User blanchet
# Date 1401703191 -7200
# Node ID c16a6264c1d829ec7e2ace31f8ee4f9903d6cd9d
# Parent  f591096a9c941d1150e63e6d98ac171a89143e5c
removed some spurious warnings in new (co)datatype package

diff -r f591096a9c94 -r c16a6264c1d8 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Jun 02 11:59:50 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Jun 02 11:59:51 2014 +0200
@@ -133,7 +133,7 @@
               val (args, size_o_mapss') = split_list (map (fn T => mk_size_of_typ T []) Ts);
               val size_const = Const (size_name, map fastype_of args ---> mk_to_natT T);
             in
-              fold (union Thm.eq_thm) (size_o_maps :: size_o_mapss')
+              fold (union Thm.eq_thm_prop) (size_o_maps :: size_o_mapss')
               #> pair (Term.list_comb (size_const, args))
             end
           | _ => pair (mk_abs_zero_nat T))
@@ -221,7 +221,8 @@
        |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm)));
 
     val nested_size_maps = map (pointfill lthy2) nested_size_o_maps @ nested_size_o_maps;
-    val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs @ nesting_bnfs);
+    val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs @ nesting_bnfs)
+      |> distinct Thm.eq_thm_prop;
 
     fun derive_size_simp size_def' simp0 =
       (trans OF [size_def', simp0])