# HG changeset patch
# User blanchet
# Date 1473593727 -7200
# Node ID fdf90aa5986835d5062f5983cff40b0e13b313c2
# Parent  2f9ee7d85d85733f9930dbd69ae1fbccbcc451f6
provide a mechanism for ensuring dead type variables occur in typedef if desired

diff -r 2f9ee7d85d85 -r fdf90aa59868 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sun Sep 11 13:35:27 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sun Sep 11 13:35:27 2016 +0200
@@ -68,8 +68,8 @@
   val mk_repT: typ -> typ -> typ -> typ
   val mk_abs: typ -> term -> term
   val mk_rep: typ -> term -> term
-  val seal_bnf: (binding -> binding) -> unfold_set -> binding -> bool -> typ list -> BNF_Def.bnf ->
-    local_theory -> (BNF_Def.bnf * (typ list * absT_info)) * local_theory
+  val seal_bnf: (binding -> binding) -> unfold_set -> binding -> bool -> typ list -> typ list ->
+    BNF_Def.bnf -> local_theory -> (BNF_Def.bnf * (typ list * absT_info)) * local_theory
 end;
 
 structure BNF_Comp : BNF_COMP =
@@ -829,13 +829,13 @@
          @{thm type_definition.Abs_cases[OF type_definition_id_bnf_UNIV]})), lthy)
   end;
 
-fun seal_bnf qualify (unfold_set : unfold_set) b force_out_of_line Ds bnf lthy =
+fun seal_bnf qualify (unfold_set : unfold_set) b force_out_of_line Ds all_Ds bnf lthy =
   let
     val live = live_of_bnf bnf;
     val nwits = nwits_of_bnf bnf;
 
     val ((As, As'), lthy1) = apfst (`(map TFree))
-      (Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ Ds lthy));
+      (Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ all_Ds lthy));
     val (Bs, _) = apfst (map TFree) (Variable.invent_types (replicate live @{sort type}) lthy1);
 
     val ((((fs, fs'), (Rs, Rs')), (Ps, Ps')), _(*names_lthy*)) = lthy
@@ -846,7 +846,7 @@
     val repTA = mk_T_of_bnf Ds As bnf;
     val T_bind = qualify b;
     val repTA_tfrees = Term.add_tfreesT repTA [];
-    val all_TA_params_in_order = fold_rev Term.add_tfreesT Ds As';
+    val all_TA_params_in_order = fold_rev Term.add_tfreesT all_Ds As';
     val TA_params =
       (if force_out_of_line then all_TA_params_in_order
        else inter (op =) repTA_tfrees all_TA_params_in_order);
@@ -880,7 +880,7 @@
     val bd_repT = fst (dest_relT (fastype_of bnf_bd));
     val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b);
     val params = Term.add_tfreesT bd_repT [];
-    val all_deads = map TFree (fold Term.add_tfreesT Ds []);
+    val all_deads = map TFree (fold_rev Term.add_tfreesT all_Ds []);
 
     val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) =
       maybe_typedef false (bdT_bind, params, NoSyn) (HOLogic.mk_UNIV bd_repT) NONE
diff -r 2f9ee7d85d85 -r fdf90aa59868 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Sun Sep 11 13:35:27 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Sun Sep 11 13:35:27 2016 +0200
@@ -957,10 +957,12 @@
 
     val timer = time (timer "Construction of BNFs");
 
-    val ((kill_poss, _), (bnfs', ((comp_cache', unfold_set'), lthy''))) =
+    val ((kill_posss, _), (bnfs', ((comp_cache', unfold_set'), lthy''))) =
       normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs (comp_cache_unfold_set, lthy');
 
-    val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
+    val Dss = @{map 3} (fn lives => fn kill_posss => fn deads => deads @ map (nth lives) kill_posss)
+      livess kill_posss deadss;
+    val all_Dss = Dss |> force_out_of_line ? map (fn Ds' => union (op =) Ds' (map TFree Ds0));
 
     fun pre_qualify b =
       Binding.qualify false (Binding.name_of b)
@@ -968,8 +970,9 @@
       #> not (Config.get lthy'' bnf_internals) ? Binding.concealed;
 
     val ((pre_bnfs, (deadss, absT_infos)), lthy''') = lthy''
-      |> @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
-        bs (replicate (length rhsXs) (force_out_of_line orelse not (null live_phantoms))) Dss bnfs'
+      |> @{fold_map 5} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
+        bs (replicate (length rhsXs) (force_out_of_line orelse not (null live_phantoms))) Dss
+        all_Dss bnfs'
       |>> split_list
       |>> apsnd split_list;