1.1 --- a/src/HOL/Codatatype/Tools/bnf_util.ML	Thu Sep 06 02:56:21 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Thu Sep 06 11:34:05 2012 +0200
     1.3 @@ -48,6 +48,8 @@
     1.4    val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
     1.5    val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context
     1.6    val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context
     1.7 +  val mk_Freesss: string -> typ list list list -> Proof.context ->
     1.8 +    term list list list * Proof.context
     1.9    val mk_Frees': string -> typ list -> Proof.context ->
    1.10      (term list * (string * typ) list) * Proof.context
    1.11    val mk_Freess': string -> typ list list -> Proof.context ->
    1.12 @@ -272,16 +274,11 @@
    1.13  fun mk_fresh_names ctxt = (fn names => Variable.variant_fixes names ctxt) oo mk_names;
    1.14  fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x
    1.15    |>> (fn names => map2 (curry Free) names Ts);
    1.16 -fun mk_Freess x Tss ctxt =
    1.17 -  fold_map2 (fn name => fn Ts => fn ctxt => mk_fresh_names ctxt (length Ts) name)
    1.18 -    (mk_names (length Tss) x) Tss ctxt
    1.19 -  |>> (fn namess => map2 (map2 (curry Free)) namess Tss);
    1.20 +fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
    1.21 +fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss;
    1.22  fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x
    1.23    |>> (fn names => `(map Free) (names ~~ Ts));
    1.24 -fun mk_Freess' x Tss ctxt =
    1.25 -  fold_map2 (fn name => fn Ts => fn ctxt =>
    1.26 -    mk_fresh_names ctxt (length Ts) name) (mk_names (length Tss) x) Tss ctxt
    1.27 -  |>> (fn namess => map_split (`(map Free) o (op ~~)) (namess ~~ Tss));
    1.28 +fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
    1.29  
    1.30  
    1.31  (** Types **)