made N2M work with sort constraints (cf. TODO)

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 08 19:21:14 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 08 19:21:19 2014 +0200
@@ -116,7 +116,6 @@
   |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
   |> map_filter I;
 
-(* TODO: test with sort constraints on As *)
 fun mutualize_fp_sugars fp cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy0 =
   let
     val thy = Proof_Context.theory_of no_defs_lthy0;
@@ -152,7 +151,12 @@
     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) =
       no_defs_lthy0
@@ -205,8 +209,8 @@
     val kss = map (fn n => 1 upto n) ns;
     val mss = map (map length) ctr_Tsss;
 
-    val fp_eqs = map dest_TFree Xs ~~ ctrXs_repTs;
-    val key = key_of_fp_eqs fp As fpTs fp_eqs;
+    val fp_eqs = map dest_TFree Xs ~~ map unsortAT ctrXs_repTs;
+    val key = key_of_fp_eqs fp unsorted_As unsorted_fpTs fp_eqs;
   in
     (case n2m_sugar_of no_defs_lthy key of
       SOME n2m_sugar => (n2m_sugar, no_defs_lthy)
@@ -220,7 +224,7 @@
         val Type (s, Us) :: _ = fpTs;
         val killed_As' =
           (case bnf_of no_defs_lthy s of
-            NONE => As'
+            NONE => unsorted_As'
           | SOME bnf =>
             let
               val Type (_, Ts) = T_of_bnf bnf;
@@ -233,8 +237,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)) =
-          fp_bnf (construct_mutualized_fp fp cliques fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
-            no_defs_lthy0;
+          fp_bnf (construct_mutualized_fp fp cliques unsorted_fpTs fp_sugars0) fp_bs unsorted_As'
+            killed_As' fp_eqs no_defs_lthy0;
 
         val fp_abs_inverses = map #abs_inverse fp_absT_infos;
         val fp_type_definitions = map #type_definition fp_absT_infos;