# HG changeset patch
# User blanchet
# Date 1346924768 -7200
# Node ID 84e3ad0d64beaa2d37644f972775d672c7956383
# Parent  db8ce685073f667e73efe7b4f6ee67733200fad2
tuning

diff -r db8ce685073f -r 84e3ad0d64be src/HOL/Codatatype/Tools/bnf_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Thu Sep 06 11:34:05 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Thu Sep 06 11:46:08 2012 +0200
@@ -268,16 +268,13 @@
 fun mk_TFreess ns = apfst (map (map TFree)) o
   fold_map Variable.invent_types (map (fn n => replicate n (HOLogic.typeS)) ns);
 
-fun mk_names n x = if n = 1 then [x]
-  else map (fn i => x ^ string_of_int i) (1 upto n);
+fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n);
 
-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_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names;
+fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts);
 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_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
 fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;