Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed bug in code generator for let and split leading to ill-formed code.
authorberghofe
Wed, 03 Aug 2005 16:43:39 +0200
changeset 17021 1c361a3de73d
parent 17020 f3014afac46f
child 17022 b257300c3a9c
Fixed bug in code generator for let and split leading to ill-formed code.
src/HOL/Product_Type.thy file | annotate | diff | comparison | revisions 
--- 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 " =>",
isabelle