# HG changeset patch
# User blanchet
# Date 1370526548 -7200
# Node ID 37a3b00759dce2b4e7ca59da0d3cb0063efb7863
# Parent  e6ed134ecd16a9efef227233571c90a099bd9343
tuning

diff -r e6ed134ecd16 -r 37a3b00759dc src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Jun 06 15:49:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Jun 06 15:49:08 2013 +0200
@@ -49,14 +49,14 @@
     typ list list list list
   val define_fold_rec:
     (typ list list * typ list list list list * term list list * term list list list list) list ->
-    (string -> binding) -> typ list -> typ list -> term -> term -> Proof.context ->
+    (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
     (term * term * thm * thm) * Proof.context
   val define_unfold_corec: term list * term list list
       * ((term list list * term list list list list * term list list list list)
          * (typ list * typ list list list * typ list list))
       * ((term list list * term list list list list * term list list list list)
          * (typ list * typ list list list * typ list list)) ->
-    (string -> binding) -> typ list -> typ list -> term -> term -> Proof.context ->
+    (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
     (term * term * thm * thm) * Proof.context
   val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list list ->
     (typ list list * typ list list list list * term list list * term list list list list) list ->
@@ -473,7 +473,8 @@
     Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss)
   end;
 
-fun define_fold_rec [fold_args_types, rec_args_types] mk_binding fpTs Cs ctor_fold ctor_rec lthy0 =
+fun define_fold_rec [fold_args_types, rec_args_types] mk_binding fpTs Cs [ctor_fold, ctor_rec]
+    lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
@@ -510,7 +511,7 @@
 
 (* TODO: merge with above function? *)
 fun define_unfold_corec (cs, cpss, unfold_args_types, corec_args_types) mk_binding fpTs Cs
-    dtor_unfold dtor_corec lthy0 =
+    [dtor_unfold, dtor_corec] lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
@@ -1319,7 +1320,7 @@
          ##>>
            (if fp = Least_FP then define_fold_rec (the fold_rec_args_types)
             else define_unfold_corec (the unfold_corec_args_types))
-             mk_binding fpTs Cs xtor_un_fold xtor_co_rec
+             mk_binding fpTs Cs [xtor_un_fold, xtor_co_rec]
          #> massage_res, lthy')
       end;