# HG changeset patch
# User blanchet
# Date 1370622269 -3600
# Node ID 40136fcb5e7a5710ebfd014797dbcdc78d1994ac
# Parent  7e352bb7600915c423dc21f0fa913594a56a13ea
tuning

diff -r 7e352bb76009 -r 40136fcb5e7a src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 17:09:07 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 17:24:29 2013 +0100
@@ -58,7 +58,7 @@
     * (thm list list * Args.src list)
   val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list ->
     string * term list * term list list * ((term list list * term list list list)
-      * (typ list * typ list list list * typ list list)) list ->
+      * (typ list * typ list list)) list ->
     thm list -> thm list -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list ->
     typ list -> typ list -> int list list -> int list list -> int list -> thm list list ->
     BNF_Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> local_theory ->
@@ -826,21 +826,9 @@
               cqf
           end;
 
-        val crgsss' =
-          (fn fcoiters => fn (_, cqfsss) =>
-              map (map (map (intr_coiters fcoiters (K I) (K I)))) cqfsss)
-            (un_fold_of fcoiterss') unfold_args;
-        val cshsss' =
-          (fn fcoiters => fn (_, cqfsss) =>
-              map (map (map (intr_coiters fcoiters (curry mk_sumT) (tack z)))) cqfsss)
-            (co_rec_of fcoiterss') corec_args;
-
-(*###
-        val [crgsss', cshsss'] =
-          map2 (fn fcoiters => fn (_, cqssss, cfssss) =>
-              map2 (map2 (map2 (intr_coiters fcoiters))) cqssss cfssss)
-            fcoiterss' [unfold_args, corec_args];
-*)
+        val crgsss' = map (map (map (intr_coiters (un_fold_of fcoiterss') (K I) (K I)))) crgsss;
+        val cshsss' = map (map (map (intr_coiters (co_rec_of fcoiterss') (curry mk_sumT) (tack z))))
+          cshsss;
 
         val unfold_goalss = map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss';
         val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';