don't generate empty theorem collections

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