--- 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;