# HG changeset patch
# User blanchet
# Date 1370590139 -7200
# Node ID 8ce7fba90bb39beae0b5be8a4ebfbe158b75ef2a
# Parent  932014a2fe538d309019eb6f018c4efad4e5d511
tuning

diff -r 932014a2fe53 -r 8ce7fba90bb3 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 08:57:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 09:28:59 2013 +0200
@@ -523,9 +523,9 @@
       (map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy
   end;
 
-fun derive_induct_iters_thms_for_types pre_bnfs [ctor_folds, ctor_recs]
-    [fold_args_types, rec_args_types] ctor_induct [ctor_fold_thms, ctor_rec_thms] nesting_bnfs
-    nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss [folds, recs] [fold_defs, rec_defs] lthy =
+fun derive_induct_iters_thms_for_types pre_bnfs (ctor_iters1 :: _) [fold_args_types, rec_args_types]
+    ctor_induct [ctor_fold_thms, ctor_rec_thms] nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss
+    ctr_defss [folds, recs] [fold_defs, rec_defs] lthy =
   let
     val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
 
@@ -541,8 +541,8 @@
 
     val fp_b_names = map base_name_of_typ fpTs;
 
-    val ctor_fold_fun_Ts = mk_fp_iter_fun_types (hd ctor_folds);
-    val ctor_rec_fun_Ts = mk_fp_iter_fun_types (hd ctor_recs);
+    val ctor_fold_fun_Ts = mk_fp_iter_fun_types (un_fold_of ctor_iters1);
+    val ctor_rec_fun_Ts = mk_fp_iter_fun_types (co_rec_of ctor_iters1);
 
     val ((((ps, ps'), xsss), us'), names_lthy) =
       lthy
@@ -677,7 +677,7 @@
      (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
   end;
 
-fun derive_coinduct_coiters_thms_for_types pre_bnfs [dtor_unfolds, dtor_corecs] dtor_coinduct
+fun derive_coinduct_coiters_thms_for_types pre_bnfs (dtor_coiters1 :: _) dtor_coinduct
     dtor_strong_induct dtor_ctors [dtor_unfold_thms, dtor_corec_thms] nesting_bnfs nested_bnfs fpTs
     Cs As kss mss ns ctr_defss ctr_sugars [unfolds, corecs] [unfold_defs, corec_defs] lthy =
   let
@@ -693,8 +693,8 @@
 
     val fp_b_names = map base_name_of_typ fpTs;
 
-    val dtor_unfold_fun_Ts = mk_fp_iter_fun_types (hd dtor_unfolds);
-    val dtor_corec_fun_Ts = mk_fp_iter_fun_types (hd dtor_corecs);
+    val dtor_unfold_fun_Ts = mk_fp_iter_fun_types (un_fold_of dtor_coiters1);
+    val dtor_corec_fun_Ts = mk_fp_iter_fun_types (co_rec_of dtor_coiters1);
 
     val ctrss = map (map (mk_ctr As) o #ctrs) ctr_sugars;
     val discss = map (map (mk_disc_or_sel As) o #discs) ctr_sugars;
@@ -1101,6 +1101,7 @@
 
     val ((xtor_co_iterss', iters_args_types, coiters_args_types), lthy) =
       mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy;
+    val xtor_co_iterss = transpose xtor_co_iterss';
 
     fun define_ctrs_case_for_type ((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
               xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
@@ -1316,7 +1317,7 @@
       let
         val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs),
              (rec_thmss, rec_attrs)) =
-          derive_induct_iters_thms_for_types pre_bnfs xtor_co_iterss' (the iters_args_types)
+          derive_induct_iters_thms_for_types pre_bnfs xtor_co_iterss (the iters_args_types)
             xtor_co_induct (transpose xtor_co_iter_thmss) nesting_bnfs nested_bnfs fpTs Cs Xs
             ctrXs_Tsss ctrss ctr_defss iterss' iter_defss' lthy;
 
@@ -1353,7 +1354,7 @@
              (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs),
              (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
              (sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) =
-          derive_coinduct_coiters_thms_for_types pre_bnfs xtor_co_iterss' xtor_co_induct
+          derive_coinduct_coiters_thms_for_types pre_bnfs xtor_co_iterss xtor_co_induct
             xtor_strong_co_induct dtor_ctors (transpose xtor_co_iter_thmss) nesting_bnfs nested_bnfs
             fpTs Cs As kss mss ns ctr_defss ctr_sugars coiterss' coiter_defss' lthy;
 
@@ -1403,7 +1404,7 @@
 
     val lthy' = lthy
       |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~
-        (transpose xtor_co_iterss') ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
+        xtor_co_iterss ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
         pre_set_defss ~~ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~
         kss ~~ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~
         sel_bindingsss ~~ raw_sel_defaultsss)
diff -r 932014a2fe53 -r 8ce7fba90bb3 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Fri Jun 07 08:57:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Fri Jun 07 09:28:59 2013 +0200
@@ -28,6 +28,8 @@
 
   val morph_fp_result: morphism -> fp_result -> fp_result
   val eq_fp_result: fp_result * fp_result -> bool
+  val un_fold_of: 'a list -> 'a
+  val co_rec_of: 'a list -> 'a
 
   val time: Timer.real_timer -> string -> Timer.real_timer
 
@@ -215,6 +217,9 @@
 fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
   eq_list eq_bnf (bnfs1, bnfs2);
 
+fun un_fold_of [f, _] = f;
+fun co_rec_of [_, r] = r;
+
 val timing = true;
 fun time timer msg = (if timing
   then warning (msg ^ ": " ^ ATP_Util.string_of_time (Timer.checkRealTimer timer))