1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 02:56:21 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 11:34:05 2012 +0200
     1.3 @@ -248,7 +248,7 @@
     1.4              val ((gss, ysss), _) =
     1.5                lthy
     1.6                |> mk_Freess "f" g_Tss
     1.7 -              ||>> apfst (unflat y_Tsss) o mk_Freess "x" (flat y_Tsss);
     1.8 +              ||>> mk_Freesss "x" y_Tsss;
     1.9  
    1.10              val iter_rhs =
    1.11                fold_rev (fold_rev Term.lambda) gss

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_util.ML	Thu Sep 06 02:56:21 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Thu Sep 06 11:34:05 2012 +0200
     2.3 @@ -48,6 +48,8 @@
     2.4    val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
     2.5    val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context
     2.6    val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context
     2.7 +  val mk_Freesss: string -> typ list list list -> Proof.context ->
     2.8 +    term list list list * Proof.context
     2.9    val mk_Frees': string -> typ list -> Proof.context ->
    2.10      (term list * (string * typ) list) * Proof.context
    2.11    val mk_Freess': string -> typ list list -> Proof.context ->
    2.12 @@ -272,16 +274,11 @@
    2.13  fun mk_fresh_names ctxt = (fn names => Variable.variant_fixes names ctxt) oo mk_names;
    2.14  fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x
    2.15    |>> (fn names => map2 (curry Free) names Ts);
    2.16 -fun mk_Freess x Tss ctxt =
    2.17 -  fold_map2 (fn name => fn Ts => fn ctxt => mk_fresh_names ctxt (length Ts) name)
    2.18 -    (mk_names (length Tss) x) Tss ctxt
    2.19 -  |>> (fn namess => map2 (map2 (curry Free)) namess Tss);
    2.20 +fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
    2.21 +fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss;
    2.22  fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x
    2.23    |>> (fn names => `(map Free) (names ~~ Ts));
    2.24 -fun mk_Freess' x Tss ctxt =
    2.25 -  fold_map2 (fn name => fn Ts => fn ctxt =>
    2.26 -    mk_fresh_names ctxt (length Ts) name) (mk_names (length Tss) x) Tss ctxt
    2.27 -  |>> (fn namess => map_split (`(map Free) o (op ~~)) (namess ~~ Tss));
    2.28 +fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
    2.29  
    2.30  
    2.31  (** Types **)