# HG changeset patch
# User desharna
# Date 1413904993 -7200
# Node ID 552ccec3f00fb9e277abffb7db652325c9430bc3
# Parent  91918686994338196b4216c832135471520e861e
generate 'size_gen' for datatypes

diff -r 919186869943 -r 552ccec3f00f src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Oct 21 17:23:13 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Oct 21 17:23:13 2014 +0200
@@ -23,6 +23,7 @@
 
 val size_N = "size_";
 val sizeN = "size";
+val size_genN = "size_gen";
 val size_o_mapN = "size_o_map";
 
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
@@ -250,6 +251,7 @@
       val overloaded_size_simpss =
         map2 (map o derive_overloaded_size_simp) overloaded_size_defs' size_simpss;
       val size_thmss = map2 append size_simpss overloaded_size_simpss;
+      val size_gen_thmss = size_simpss
 
       val ABs = As ~~ Bs;
       val g_names = variant_names num_As "g";
@@ -315,6 +317,7 @@
 
       val notes =
         [(sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs),
+         (size_genN, size_gen_thmss, []),
          (size_o_mapN, size_o_map_thmss, [])]
         |> massage_multi_notes;