--- a/src/HOL/Product_Type.thy Thu Mar 03 09:22:35 2005 +0100
+++ b/src/HOL/Product_Type.thy Thu Mar 03 12:43:01 2005 +0100
@@ -816,7 +816,7 @@
val (gr1, qs) = foldl_map mk_code (gr, ps);
val (gr2, pu) = Codegen.invoke_codegen thy dep false (gr1, u)
in
- SOME (gr2, Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, flat
+ SOME (gr2, Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat
(separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
[Pretty.block [Pretty.str "val ", pl, Pretty.str " =",
Pretty.brk 1, pr]]) qs))),