src/HOL/Product_Type.thy
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 16121 a80aa66d2271
     1.1 --- a/src/HOL/Product_Type.thy	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -816,7 +816,7 @@
     1.4              val (gr1, qs) = foldl_map mk_code (gr, ps);
     1.5              val (gr2, pu) = Codegen.invoke_codegen thy dep false (gr1, u)
     1.6            in
     1.7 -            SOME (gr2, Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, flat
     1.8 +            SOME (gr2, Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat
     1.9                  (separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
    1.10                    [Pretty.block [Pretty.str "val ", pl, Pretty.str " =",
    1.11                       Pretty.brk 1, pr]]) qs))),