honour sorts in N2M

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 08 16:51:35 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 08 19:21:07 2014 +0200
@@ -1187,7 +1187,7 @@
       end;
 
     val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of_spec) specs;
-    val unsorted_Ass0 = map (map (resort_tfree @{sort type})) Ass0;
+    val unsorted_Ass0 = map (map (resort_tfree_or_tvar @{sort type})) Ass0;
     val unsorted_As = Library.foldr1 (merge_type_args fp) unsorted_Ass0;
     val num_As = length unsorted_As;
 
@@ -1196,7 +1196,7 @@
 
     val ((((Bs0, Cs as C1 :: _), Es as E1 :: _), Xs), no_defs_lthy) =
       no_defs_lthy0
-      |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
+      |> fold (Variable.declare_typ o resort_tfree_or_tvar dummyS) unsorted_As
       |> mk_TFrees num_As
       ||>> mk_TFrees nn
       ||>> mk_TFrees nn
@@ -1340,7 +1340,8 @@
         ();
 
     val Bs =
-      map3 (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree S B else A)
+      map3 (fn alive => fn A as TFree (_, S) => fn B =>
+          if alive then resort_tfree_or_tvar S B else A)
         (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0;
 
     val B_ify = Term.typ_subst_atomic (As ~~ Bs);

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 08 16:51:35 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 08 19:21:07 2014 +0200
@@ -370,7 +370,7 @@
     fun gather_types _ _ rev_seens gen_seen [] = (rev rev_seens, gen_seen)
       | gather_types lthy rho rev_seens gen_seen ((T as Type (_, tyargs)) :: Ts) =
         let
-          val {fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T;
+          val {T = Type (_, tyargs0), fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T;
           val mutual_Ts = map (retypargs tyargs) mutual_Ts0;
 
           val rev_seen = flat rev_seens;
@@ -379,9 +379,11 @@
 
           fun fresh_tyargs () =
             let
-              val (gen_tyargs, lthy') =
+              val (unsorted_gen_tyargs, lthy') =
                 variant_tfrees (replicate (length tyargs) "a") lthy
                 |>> map Logic.varifyT_global;
+              val gen_tyargs =
+                map2 (resort_tfree_or_tvar o snd o dest_TFree_or_TVar) tyargs0 unsorted_gen_tyargs;
               val rho' = (gen_tyargs ~~ tyargs) @ rho;
             in
               (rho', gen_tyargs, gen_seen, lthy')

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 08 16:51:35 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 08 19:21:07 2014 +0200
@@ -393,7 +393,7 @@
       |> variant_tfrees (map (fst o dest_TFree_or_TVar) As0)
       ||> the_single o fst o mk_TFrees 1;
 
-    val As = map2 (resort_tfree o snd o dest_TFree_or_TVar) As0 unsorted_As;
+    val As = map2 (resort_tfree_or_tvar o snd o dest_TFree_or_TVar) As0 unsorted_As;
 
     val fcT = Type (fcT_name, As);
     val ctrs = map (mk_ctr As) ctrs0;

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Sep 08 16:51:35 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Sep 08 19:21:07 2014 +0200
@@ -35,7 +35,7 @@
   val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context
   val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context
   val dest_TFree_or_TVar: typ -> string * sort
-  val resort_tfree: sort -> typ -> typ
+  val resort_tfree_or_tvar: sort -> typ -> typ
   val variant_types: string list -> sort list -> Proof.context ->
     (string * sort) list * Proof.context
   val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
@@ -182,7 +182,8 @@
   | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
   | dest_TFree_or_TVar _ = error "Invalid type argument";
 
-fun resort_tfree S (TFree (s, _)) = TFree (s, S);
+fun resort_tfree_or_tvar S (TFree (s, _)) = TFree (s, S)
+  | resort_tfree_or_tvar S (TVar (x, _)) = TVar (x, S);
 
 fun ensure_prefix pre s = s |> not (String.isPrefix pre s) ? prefix pre;
 

--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Sep 08 16:51:35 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Sep 08 19:21:07 2014 +0200
@@ -314,7 +314,7 @@
     val liveness =
       BNF_FP_Def_Sugar.liveness_of_fp_bnf (length old_As) (hd (#bnfs (#fp_res fp_sugar)));
     val (unsorted_As, lthy) = mk_TFrees live lthy
-    val As = map2 (Ctr_Sugar_Util.resort_tfree o snd o Ctr_Sugar_Util.dest_TFree_or_TVar)
+    val As = map2 (Ctr_Sugar_Util.resort_tfree_or_tvar o snd o Ctr_Sugar_Util.dest_TFree_or_TVar)
       (map_filter (uncurry (fn true => SOME | false => K NONE)) (liveness ~~ old_As)) unsorted_As
     val predTs = map mk_pred1T As
     val (preds, lthy) = mk_Frees "P" predTs lthy