src/HOL/Product_Type.thy
changeset 17021 1c361a3de73d
parent 17002 fb9261990ffe
child 17085 5b57f995a179
--- 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 " =>",