diff -r 1b3115d1a8df -r 8d8c70b41bab src/HOL/Product_Type.thy
--- 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))),