# HG changeset patch
# User blanchet
# Date 1367932284 -7200
# Node ID c2c23ac31973992bd2c8205c19cfee367d283b38
# Parent  3cc73166bbc533ff9e619c280526159b4dfb958a
code tuning

diff -r 3cc73166bbc5 -r c2c23ac31973 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 15:03:15 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 15:11:24 2013 +0200
@@ -471,13 +471,13 @@
 
 fun define_fold_rec fold_only rec_only mk_binding fpTs As Cs ctor_fold ctor_rec no_defs_lthy =
   let
-    val kk = find_index (curry (op =) (body_type (fastype_of ctor_fold))) Cs;
-    val fpT = nth fpTs kk; (* ### can use dummyT? or steal it from ctor_fold etc? *)
-    val C = nth Cs kk;
+    val nn = length fpTs;
+
+    val fpT_to_C = snd (strip_typeN nn (fastype_of ctor_fold));
 
     fun generate_iter (suf, ctor_iter, (fss, f_Tss, xsss)) =
       let
-        val res_T = fold_rev (curry (op --->)) f_Tss (fpT --> C);
+        val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
         val binding = mk_binding suf;
         val spec =
           mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)),
@@ -505,14 +505,14 @@
 fun define_unfold_corec cs ns cpss unfold_only corec_only mk_binding fpTs As Cs dtor_unfold
     dtor_corec no_defs_lthy =
   let
-    val kk = find_index (curry (op =) (body_type (fastype_of dtor_unfold))) fpTs;
-    val fpT = nth fpTs kk; (* ### can use dummyT? or steal it from ctor_fold etc? *)
-    val C = nth Cs kk;
+    val nn = length fpTs;
+
+    val C_to_fpT = snd (strip_typeN nn (fastype_of dtor_unfold));
 
     fun generate_coiter (suf, dtor_coiter, ((pfss, cqssss, cfssss),
         (f_sum_prod_Ts, f_Tsss, pf_Tss))) =
       let
-        val res_T = fold_rev (curry (op --->)) pf_Tss (C --> fpT);
+        val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT;
         val binding = mk_binding suf;
         val spec =
           mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)),