# HG changeset patch
# User blanchet
# Date 1367918849 -7200
# Node ID e5432ec161ff1241f2bf2367ecc482bf31f7c1c1
# Parent  b4e85748ce484bfe657dc1d6917cf75b52b70119
tuned names + extended ML signature

diff -r b4e85748ce48 -r e5432ec161ff src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 10:35:40 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 11:27:29 2013 +0200
@@ -25,13 +25,14 @@
 
   val exists_subtype_in: typ list -> typ -> bool
   val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c
+  val mk_fp_iter: bool -> typ list -> typ list -> term list -> term list * typ list
   val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term
 
   val mk_iter_fun_arg_types_pairsss: typ list -> int list -> int list list -> term ->
     (typ list * typ list) list list list
-  val mk_fold_recs: Proof.context -> typ list -> typ list -> typ list -> int list ->
+  val mk_folds_recs: Proof.context -> typ list -> typ list -> typ list -> int list ->
     int list list -> term list -> term list -> term list * term list
-  val mk_unfold_corecs: Proof.context -> typ list -> typ list -> typ list -> int list ->
+  val mk_unfolds_corecs: Proof.context -> typ list -> typ list -> typ list -> int list ->
     int list list -> term list -> term list -> term list * term list
 
   val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm ->
@@ -405,7 +406,7 @@
     Term.list_comb (ctor_iter, map2 (mk_sum_caseN_balanced oo map2 mk_iter_arg) fss xsss)
   end;
 
-fun mk_fold_recs lthy fpTs As Cs ns mss ctor_folds ctor_recs =
+fun mk_folds_recs lthy fpTs As Cs ns mss ctor_folds ctor_recs =
   let
     val (_, ctor_fold_fun_Ts) = mk_fp_iter true As Cs ctor_folds;
     val (_, ctor_rec_fun_Ts) = mk_fp_iter true As Cs ctor_recs;
@@ -439,7 +440,7 @@
     Term.list_comb (dtor_coiter, map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss)
   end;
 
-fun mk_unfold_corecs lthy fpTs As Cs ns mss dtor_unfolds dtor_corecs =
+fun mk_unfolds_corecs lthy fpTs As Cs ns mss dtor_unfolds dtor_corecs =
   let
     val (_, dtor_unfold_fun_Ts) = mk_fp_iter true As Cs dtor_unfolds;
     val (_, dtor_corec_fun_Ts) = mk_fp_iter true As Cs dtor_corecs;