1.1 --- a/src/HOL/Codatatype/Tools/bnf_util.ML	Thu Sep 06 11:34:05 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Thu Sep 06 11:46:08 2012 +0200
     1.3 @@ -268,16 +268,13 @@
     1.4  fun mk_TFreess ns = apfst (map (map TFree)) o
     1.5    fold_map Variable.invent_types (map (fn n => replicate n (HOLogic.typeS)) ns);
     1.6  
     1.7 -fun mk_names n x = if n = 1 then [x]
     1.8 -  else map (fn i => x ^ string_of_int i) (1 upto n);
     1.9 +fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n);
    1.10  
    1.11 -fun mk_fresh_names ctxt = (fn names => Variable.variant_fixes names ctxt) oo mk_names;
    1.12 -fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x
    1.13 -  |>> (fn names => map2 (curry Free) names Ts);
    1.14 +fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names;
    1.15 +fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts);
    1.16  fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
    1.17  fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss;
    1.18 -fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x
    1.19 -  |>> (fn names => `(map Free) (names ~~ Ts));
    1.20 +fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
    1.21  fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
    1.22  
    1.23