# HG changeset patch
# User blanchet
# Date 1393192271 -3600
# Node ID 38f75365fc2a977e4c1663536bbd507177088d2f
# Parent  cf6a029b28d8cf6736b25ab8a58b7178dd542807
added explicit killing

diff -r cf6a029b28d8 -r 38f75365fc2a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Feb 23 22:51:11 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Feb 23 22:51:11 2014 +0100
@@ -1057,12 +1057,16 @@
       | extras => List.app (fn extra => warning ("Unused type variable on right-hand side of " ^
           co_prefix fp ^ "datatype definition: " ^ qsoty (TFree extra))) extras);
 
+    val killed_As =
+      map_filter (fn (A, set_bos) => if exists is_none set_bos then SOME A else NONE)
+        (unsorted_As ~~ transpose set_boss);
+
     val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0,
            xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects,
            dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...},
            lthy)) =
-      fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
-        no_defs_lthy0
+      fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
+        (map dest_TFree killed_As) fp_eqs no_defs_lthy0
       handle BAD_DEAD (X, X_backdrop) =>
         (case X_backdrop of
           Type (bad_tc, _) =>
diff -r cf6a029b28d8 -r 38f75365fc2a src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- 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
@@ -199,7 +199,7 @@
 
         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' fp_eqs no_defs_lthy;
+          fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' [](*### FIXME*) fp_eqs no_defs_lthy;
 
         val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
         val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
diff -r cf6a029b28d8 -r 38f75365fc2a src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Sun Feb 23 22:51:11 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Sun Feb 23 22:51:11 2014 +0100
@@ -180,8 +180,8 @@
 
   val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> local_theory -> 'a) ->
-    binding list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory ->
-    BNF_Def.bnf list * 'a
+    binding list -> (string * sort) list -> (string * sort) list -> ((string * sort) * typ) list ->
+    local_theory -> BNF_Def.bnf list * 'a
 end;
 
 structure BNF_FP_Util : BNF_FP_UTIL =
@@ -562,7 +562,7 @@
     |> unfold_thms ctxt unfolds
   end;
 
-fun fp_bnf construct_fp bs resBs fp_eqs lthy =
+fun fp_bnf construct_fp bs resBs Ds0 fp_eqs lthy =
   let
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
@@ -590,7 +590,7 @@
 
     val Ass = map (map dest_TFree) livess;
     val resDs = fold (subtract (op =)) Ass resBs;
-    val Ds = fold (fold Term.add_tfreesT) deadss [];
+    val Ds = fold (fold Term.add_tfreesT) deadss Ds0;
 
     val timer = time (timer "Construction of BNFs");