--- 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)
--- 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;
--- 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