# HG changeset patch
# User traytel
# Date 1469536160 -7200
# Node ID 679402a894aeff991c7a7945f75432cd9a01b9d8
# Parent  3a0f40a6fa42362ea4a7e90e44cd4becea25fe37
honor sorts in (co)datatype declarations

diff -r 3a0f40a6fa42 -r 679402a894ae src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jul 26 10:33:39 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jul 26 14:29:20 2016 +0200
@@ -2148,11 +2148,11 @@
         warn (order_strong_conn (op =) Int_Graph.make Int_Graph.topological_order deps sccs)
       end;
 
-    val fp_eqs = map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs;
+    val fp_eqs = map dest_TFree Xs ~~ ctrXs_repTs;
 
     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);
+        (As ~~ transpose set_boss);
 
     val (((pre_bnfs, absT_infos), _), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
              dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
@@ -2161,7 +2161,7 @@
              xtor_co_rec_transfers, xtor_co_rec_o_maps, ...},
            lthy)) =
       fixpoint_bnf I (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs
-        (map dest_TFree unsorted_As) (map dest_TFree killed_As) fp_eqs empty_comp_cache no_defs_lthy
+        (map dest_TFree As) (map dest_TFree killed_As) fp_eqs empty_comp_cache no_defs_lthy
       handle BAD_DEAD (X, X_backdrop) =>
         (case X_backdrop of
           Type (bad_tc, _) =>
diff -r 3a0f40a6fa42 -r 679402a894ae src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Jul 26 10:33:39 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Jul 26 14:29:20 2016 +0200
@@ -157,12 +157,7 @@
     val ctr_Tss = map (map fastype_of) ctrss;
 
     val As' = fold (fold Term.add_tfreesT) ctr_Tss [];
-    val unsorted_As' = map (apsnd (K @{sort type})) As';
     val As = map TFree As';
-    val unsorted_As = map TFree unsorted_As';
-
-    val unsortAT = Term.typ_subst_atomic (As ~~ unsorted_As);
-    val unsorted_fpTs = map unsortAT fpTs;
 
     val ((Cs, Xs), _) =
       no_defs_lthy
@@ -217,8 +212,8 @@
     val kss = map (fn n => 1 upto n) ns;
     val mss = map (map length) ctr_Tsss;
 
-    val fp_eqs = map dest_TFree Xs ~~ map unsortAT ctrXs_repTs;
-    val key = key_of_fp_eqs fp unsorted_As unsorted_fpTs fp_eqs;
+    val fp_eqs = map dest_TFree Xs ~~ ctrXs_repTs;
+    val key = key_of_fp_eqs fp As fpTs fp_eqs;
   in
     (case n2m_sugar_of no_defs_lthy key of
       SOME n2m_sugar => (n2m_sugar, no_defs_lthy)
@@ -232,7 +227,7 @@
         val Type (s, Us) :: _ = fpTs;
         val killed_As' =
           (case bnf_of no_defs_lthy s of
-            NONE => unsorted_As'
+            NONE => As'
           | SOME bnf =>
             let
               val Type (_, Ts) = T_of_bnf bnf;
@@ -246,8 +241,8 @@
 
         val (((pre_bnfs, absT_infos), _), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
                dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
-          fixpoint_bnf I (construct_mutualized_fp fp mutual_cliques unsorted_fpTs indexed_fp_ress)
-            fp_bs unsorted_As' killed_As' fp_eqs empty_comp_cache no_defs_lthy;
+          fixpoint_bnf I (construct_mutualized_fp fp mutual_cliques fpTs indexed_fp_ress)
+            fp_bs As' killed_As' fp_eqs empty_comp_cache no_defs_lthy;
 
         val time = time lthy;
         val timer = time (Timer.startRealTimer ());