# HG changeset patch
# User kuncar
# Date 1413820581 -7200
# Node ID f9a966c834bc4f436d833558bf7d01a7d5a5b999
# Parent  e4f4925d4a9dccc716bc2cf804a1af58a26f20c1
refactored

diff -r e4f4925d4a9d -r f9a966c834bc src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Oct 20 17:41:04 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Oct 20 17:56:21 2014 +0200
@@ -304,6 +304,16 @@
     SOME data => data
     | NONE => (error "lookup_pred_data: something went utterly wrong")
 
+fun lives_of_fp fp_sugar =
+  let
+    val As = snd (dest_Type (#T fp_sugar))
+    val liveness = liveness_of_fp_bnf (length As) (hd (#bnfs (#fp_res fp_sugar)));
+  in
+    map_filter (uncurry (fn true => SOME | false => K NONE)) (liveness ~~ As)
+  end
+
+fun sorts_of_fp fp_sugar = map (snd o Ctr_Sugar_Util.dest_TFree_or_TVar) (lives_of_fp fp_sugar)
+
 fun prove_pred_inject lthy (fp_sugar:fp_sugar) =
   let
     val involved_types = distinct op= (
@@ -311,14 +321,8 @@
       @ map type_name_of_bnf (#live_nesting_bnfs fp_sugar)
       @ map type_name_of_bnf (#bnfs (#fp_res fp_sugar)))
     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 old_As = snd (dest_Type (#T fp_sugar))
-    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_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 (As, lthy) = mk_TFrees' (sorts_of_fp fp_sugar) lthy
     val predTs = map mk_pred1T As
     val (preds, lthy) = mk_Frees "P" predTs lthy
     val args = map mk_eq_onp preds