# HG changeset patch
# User blanchet
# Date 1410181897 -7200
# Node ID d91f7a80f41271991cb3956b40645f8e7e462421
# Parent  04faf6dc262e3ff127b06ea493c79ed65a779d52
use right sort constraints

diff -r 04faf6dc262e -r d91f7a80f412 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 08 14:04:03 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 08 15:11:37 2014 +0200
@@ -388,10 +388,6 @@
 
     fun qualify mandatory = Binding.qualify mandatory fc_b_name;
 
-    fun dest_TFree_or_TVar (TFree sS) = sS
-      | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
-      | dest_TFree_or_TVar _ = error "Invalid type argument";
-
     val (unsorted_As, B) =
       no_defs_lthy
       |> variant_tfrees (map (fst o dest_TFree_or_TVar) As0)
diff -r 04faf6dc262e -r d91f7a80f412 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Sep 08 14:04:03 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Sep 08 15:11:37 2014 +0200
@@ -34,6 +34,7 @@
     (term list list * (string * typ) list list) * Proof.context
   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 variant_types: string list -> sort list -> Proof.context ->
     (string * sort) list * Proof.context
@@ -177,6 +178,10 @@
 fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts);
 fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
 
+fun dest_TFree_or_TVar (TFree sS) = sS
+  | 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 ensure_prefix pre s = s |> not (String.isPrefix pre s) ? prefix pre;
diff -r 04faf6dc262e -r d91f7a80f412 src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Sep 08 14:04:03 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Sep 08 15:11:37 2014 +0200
@@ -310,7 +310,10 @@
     val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types
     val live = live_of_bnf (bnf_of_fp_sugar fp_sugar)
     val old_lthy = lthy
-    val (As, lthy) = mk_TFrees live lthy
+    val old_As = snd (dest_Type (#T 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)
+      old_As unsorted_As
     val predTs = map mk_pred1T As
     val (preds, lthy) = mk_Frees "P" predTs lthy
     val args = map mk_eq_onp preds