src/HOL/Tools/BNF/bnf_fp_util.ML

 
   val mk_strong_coinduct_thm: thm -> thm list -> thm list -> Proof.context -> thm
 
   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 =
 struct
 

   in
     Thm.instantiate ([], insts) coind
     |> 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 ());
     val (Xs, rhsXs) = split_list fp_eqs;
 

     fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
       #> Binding.conceal;
 
     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");
 
     val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) =
       normalize_bnfs norm_qualify Ass Ds fp_sort bnfs unfold_set lthy;