# HG changeset patch
# User blanchet
# Date 1346924045 -7200
# Node ID db8ce685073f667e73efe7b4f6ee67733200fad2
# Parent  6d29d2db5f88c211e53348eb2e51c9293c60b05f
introduced and used "mk_Freesss", and simplified "mk_Freess(')"

diff -r 6d29d2db5f88 -r db8ce685073f src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 02:56:21 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 11:34:05 2012 +0200
@@ -248,7 +248,7 @@
             val ((gss, ysss), _) =
               lthy
               |> mk_Freess "f" g_Tss
-              ||>> apfst (unflat y_Tsss) o mk_Freess "x" (flat y_Tsss);
+              ||>> mk_Freesss "x" y_Tsss;
 
             val iter_rhs =
               fold_rev (fold_rev Term.lambda) gss
diff -r 6d29d2db5f88 -r db8ce685073f src/HOL/Codatatype/Tools/bnf_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Thu Sep 06 02:56:21 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Thu Sep 06 11:34:05 2012 +0200
@@ -48,6 +48,8 @@
   val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
   val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context
   val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context
+  val mk_Freesss: string -> typ list list list -> Proof.context ->
+    term list list list * Proof.context
   val mk_Frees': string -> typ list -> Proof.context ->
     (term list * (string * typ) list) * Proof.context
   val mk_Freess': string -> typ list list -> Proof.context ->
@@ -272,16 +274,11 @@
 fun mk_fresh_names ctxt = (fn names => Variable.variant_fixes names ctxt) oo mk_names;
 fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x
   |>> (fn names => map2 (curry Free) names Ts);
-fun mk_Freess x Tss ctxt =
-  fold_map2 (fn name => fn Ts => fn ctxt => mk_fresh_names ctxt (length Ts) name)
-    (mk_names (length Tss) x) Tss ctxt
-  |>> (fn namess => map2 (map2 (curry Free)) namess Tss);
+fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
+fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss;
 fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x
   |>> (fn names => `(map Free) (names ~~ Ts));
-fun mk_Freess' x Tss ctxt =
-  fold_map2 (fn name => fn Ts => fn ctxt =>
-    mk_fresh_names ctxt (length Ts) name) (mk_names (length Tss) x) Tss ctxt
-  |>> (fn namess => map_split (`(map Free) o (op ~~)) (namess ~~ Tss));
+fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
 
 
 (** Types **)