src/HOL/Product_Type.thy
changeset 17021 1c361a3de73d
parent 17002 fb9261990ffe
child 17085 5b57f995a179
equal deleted inserted replaced
17020:f3014afac46f 17021:1c361a3de73d
   817       | (ps, u) =>
   817       | (ps, u) =>
   818           let
   818           let
   819             val (gr1, qs) = foldl_map mk_code (gr, ps);
   819             val (gr1, qs) = foldl_map mk_code (gr, ps);
   820             val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
   820             val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
   821             val (gr3, pargs) = foldl_map
   821             val (gr3, pargs) = foldl_map
   822               (Codegen.invoke_codegen thy defs dep thyname false) (gr2, ts)
   822               (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
   823           in
   823           in
   824             SOME (gr3, Codegen.mk_app brack
   824             SOME (gr3, Codegen.mk_app brack
   825               (Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat
   825               (Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat
   826                   (separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
   826                   (separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
   827                     [Pretty.block [Pretty.str "val ", pl, Pretty.str " =",
   827                     [Pretty.block [Pretty.str "val ", pl, Pretty.str " =",
   838          ([p], u) =>
   838          ([p], u) =>
   839            let
   839            let
   840              val (gr1, q) = Codegen.invoke_codegen thy defs dep thyname false (gr, p);
   840              val (gr1, q) = Codegen.invoke_codegen thy defs dep thyname false (gr, p);
   841              val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
   841              val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
   842              val (gr3, pargs) = foldl_map
   842              val (gr3, pargs) = foldl_map
   843                (Codegen.invoke_codegen thy defs dep thyname false) (gr2, ts)
   843                (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
   844            in
   844            in
   845              SOME (gr2, Codegen.mk_app brack
   845              SOME (gr2, Codegen.mk_app brack
   846                (Pretty.block [Pretty.str "(fn ", q, Pretty.str " =>",
   846                (Pretty.block [Pretty.str "(fn ", q, Pretty.str " =>",
   847                  Pretty.brk 1, pu, Pretty.str ")"]) pargs)
   847                  Pretty.brk 1, pu, Pretty.str ")"]) pargs)
   848            end
   848            end