# HG changeset patch
# User blanchet
# Date 1473593727 -7200
# Node ID 2f9ee7d85d85733f9930dbd69ae1fbccbcc451f6
# Parent  4f8c6e63bc41aa92892760a77b849917e3f8fa4e
preserve order of dead variables

diff -r 4f8c6e63bc41 -r 2f9ee7d85d85 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sun Sep 11 13:35:25 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sun Sep 11 13:35:27 2016 +0200
@@ -845,10 +845,11 @@
 
     val repTA = mk_T_of_bnf Ds As bnf;
     val T_bind = qualify b;
-    val all_TA_params_in_order = Term.add_tfreesT repTA As';
+    val repTA_tfrees = Term.add_tfreesT repTA [];
+    val all_TA_params_in_order = fold_rev Term.add_tfreesT Ds As';
     val TA_params =
       (if force_out_of_line then all_TA_params_in_order
-       else inter (op =) (Term.add_tfreesT repTA []) all_TA_params_in_order);
+       else inter (op =) repTA_tfrees all_TA_params_in_order);
     val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
       maybe_typedef force_out_of_line (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
         (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;