# HG changeset patch
# User blanchet
# Date 1367868556 -7200
# Node ID cc60613a15285ef2cab918b94a117bf1974f3de6
# Parent  2928fda12661fc9c81a6ef71f2512556bc16f022
rationalize ML signature

diff -r 2928fda12661 -r cc60613a1528 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon May 06 21:20:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon May 06 21:29:16 2013 +0200
@@ -27,11 +27,8 @@
   val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c
   val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term
 
-  val mk_fp_iter_fun_types: term -> typ list
-  val mk_fun_arg_typess: int -> int list -> typ -> typ list list
-  val unzip_recT: typ list -> typ -> typ list * typ list
-  val mk_fold_fun_typess: typ list list list -> typ list list -> typ list list
-  val mk_rec_fun_typess: typ list -> typ list list list -> typ list list -> typ list list
+  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 ->
     int list list -> term list -> term list -> term list * term list
 
@@ -237,6 +234,11 @@
 
 fun mk_fun_arg_typess n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
 
+fun mk_iter_fun_arg_types_pairsss fpTs ns mss =
+  mk_fp_iter_fun_types
+  #> map3 mk_fun_arg_typess ns mss
+  #> map (map (map (unzip_recT fpTs)));
+
 fun mk_fold_rec_args_types fpTs Css ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy =
   let
     val y_Tsss = map3 mk_fun_arg_typess ns mss ctor_fold_fun_Ts;