--- a/src/HOL/Product_Type.thy Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Product_Type.thy Thu Oct 15 23:28:10 2009 +0200
@@ -1017,7 +1017,7 @@
(Codegen.invoke_codegen thy defs dep thyname true) ts gr2
in
SOME (Codegen.mk_app brack
- (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, List.concat
+ (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat
(separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
[Pretty.block [Codegen.str "val ", pl, Codegen.str " =",
Pretty.brk 1, pr]]) qs))),