allow sorts on dead variables in BNFs

--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Apr 28 22:56:50 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Apr 28 22:57:07 2015 +0200
@@ -777,7 +777,7 @@
             Dont_Inline => false
           | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
           | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_term_size
-          | Do_Inline => true)
+          | Do_Inline => true);
       in
         if inline then
           ((rhs, Drule.reflexive_thm), lthy)
@@ -861,13 +861,16 @@
     fun mk_bnf_t Ds As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As'));
     fun mk_bnf_T Ds As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As'));
 
-    val (((As, Bs), Ds), names_lthy) = lthy
+    val (((As, Bs), unsorted_Ds), names_lthy) = lthy
       |> mk_TFrees live
       ||>> mk_TFrees live
       ||>> mk_TFrees (length deads);
+
+    val Ds = map2 (resort_tfree_or_tvar o Type.sort_of_atyp) deads unsorted_Ds;
+
     val RTs = map2 (curry HOLogic.mk_prodT) As Bs;
     val pred2RTs = map2 mk_pred2T As Bs;
-    val (Rs, Rs') = names_lthy |> mk_Frees' "R" pred2RTs |> fst
+    val (Rs, Rs') = names_lthy |> mk_Frees' "R" pred2RTs |> fst;
     val CA = mk_bnf_T Ds As Calpha;
     val CR = mk_bnf_T Ds RTs Calpha;
     val setRs =
@@ -967,7 +970,7 @@
 
     val dead = length deads;
 
-    val (((((((As', Bs'), Cs), Ds), Es), B1Ts), B2Ts), (Ts, T)) = lthy
+    val (((((((As', Bs'), Cs), unsorted_Ds), Es), B1Ts), B2Ts), (Ts, T)) = lthy
       |> mk_TFrees live
       ||>> mk_TFrees live
       ||>> mk_TFrees live
@@ -979,6 +982,8 @@
       ||> the_single
       ||> `(replicate live);
 
+    val Ds = map2 (resort_tfree_or_tvar o Type.sort_of_atyp) deads unsorted_Ds;
+
     val mk_bnf_map = mk_bnf_map_Ds Ds;
     val mk_bnf_t = mk_bnf_t_Ds Ds;
     val mk_bnf_T = mk_bnf_T_Ds Ds;