# HG changeset patch
# User blanchet
# Date 1427446377 -3600
# Node ID fd3a7692e08301b45f97804f48d83dee8d133f65
# Parent  0e9a0a5f4424649eaa7d068b6efc4ffaf47a3954
preserve order of type arguments in pre-FP BNF typedef

diff -r 0e9a0a5f4424 -r fd3a7692e083 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Mar 26 23:23:04 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Fri Mar 27 09:52:57 2015 +0100
@@ -791,7 +791,10 @@
 
     val repTA = mk_T_of_bnf Ds As bnf;
     val T_bind = qualify b;
-    val TA_params = Term.add_tfreesT repTA (if has_live_phantoms then As' else []);
+    val all_TA_params_in_order = Term.add_tfreesT repTA As';
+    val TA_params =
+      (if has_live_phantoms then all_TA_params_in_order
+       else inter (op =) (Term.add_tfreesT repTA []) all_TA_params_in_order);
     val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
       maybe_typedef lthy has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
         (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;