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