# HG changeset patch
# User berghofe
# Date 1123080219 -7200
# Node ID 1c361a3de73da1c3754a63f25086b215acb7ad75
# Parent  f3014afac46f825e8edac3abf85138240cbac976
Fixed bug in code generator for let and split leading to ill-formed code.

diff -r f3014afac46f -r 1c361a3de73d src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Aug 03 16:28:22 2005 +0200
+++ b/src/HOL/Product_Type.thy	Wed Aug 03 16:43:39 2005 +0200
@@ -819,7 +819,7 @@
             val (gr1, qs) = foldl_map mk_code (gr, ps);
             val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
             val (gr3, pargs) = foldl_map
-              (Codegen.invoke_codegen thy defs dep thyname false) (gr2, ts)
+              (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
           in
             SOME (gr3, Codegen.mk_app brack
               (Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat
@@ -840,7 +840,7 @@
              val (gr1, q) = Codegen.invoke_codegen thy defs dep thyname false (gr, p);
              val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
              val (gr3, pargs) = foldl_map
-               (Codegen.invoke_codegen thy defs dep thyname false) (gr2, ts)
+               (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
            in
              SOME (gr2, Codegen.mk_app brack
                (Pretty.block [Pretty.str "(fn ", q, Pretty.str " =>",