improved accounting for dead variables when naming set functions (refines d71c2737ee21)

--- a/src/HOL/BNF_FP_Base.thy	Sun Feb 23 22:51:11 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy	Sun Feb 23 22:51:11 2014 +0100
@@ -154,5 +154,5 @@
 ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
 ML_file "Tools/BNF/bnf_fp_n2m.ML"
 ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
- 
+
 end

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Sun Feb 23 22:51:11 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Sun Feb 23 22:51:11 2014 +0100
@@ -197,9 +197,22 @@
             Binding.qualify true b_name (Binding.name (n2mN ^ base_fp_name)))
           b_names base_fp_names;
 
+        val Type (s, Us) :: _ = fpTs;
+        val killed_As' =
+          (case bnf_of no_defs_lthy s of
+            NONE => As'
+          | SOME bnf =>
+            let
+              val Type (_, Ts) = T_of_bnf bnf;
+              val deads = deads_of_bnf bnf;
+              val dead_Us =
+                map_filter (fn (T, U) => if member (op =) deads T then SOME U else NONE) (Ts ~~ Us);
+            in fold Term.add_tfreesT dead_Us [] end);
+
         val (pre_bnfs, (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_injects,
                dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
-          fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' [](*### FIXME*) fp_eqs no_defs_lthy;
+          fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
+            no_defs_lthy;
 
         val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
         val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;

--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Sun Feb 23 22:51:11 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Sun Feb 23 22:51:11 2014 +0100
@@ -1406,7 +1406,7 @@
 
         val set_bss =
           map (flat o map2 (fn B => fn b =>
-            if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0;
+            if member (op =) deads (TFree B) then [] else [b]) resBs) set_bss0;
 
         val ctor_witss =
           let