# HG changeset patch # User blanchet # Date 1379925077 -7200 # Node ID f0b273258d8005afad7c06308df1b533538e5fb8 # Parent 0ddf045113c93e780b8fa6f17e2d1c548bc9503c don't generate empty theorem collections diff -r 0ddf045113c9 -r f0b273258d80 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Sep 23 10:30:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Sep 23 10:31:17 2013 +0200 @@ -1229,12 +1229,10 @@ val massage_multi_notes = maps (fn (thmN, thmss, attrs) => - if forall null thmss then - [] - else - map3 (fn fp_b_name => fn Type (T_name, _) => fn thms => - ((qualify true fp_b_name (Binding.name thmN), attrs T_name), [(thms, [])])) - fp_b_names fpTs thmss); + map3 (fn fp_b_name => fn Type (T_name, _) => fn thms => + ((qualify true fp_b_name (Binding.name thmN), attrs T_name), [(thms, [])])) + fp_b_names fpTs thmss) + #> filter_out (null o fst o hd o snd); val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss; val ns = map length ctr_Tsss;