src/HOL/Product_Type.thy
changeset 26975 103dca19ef2e
parent 26798 a9134a089106
child 27104 791607529f6d
     1.1 --- a/src/HOL/Product_Type.thy	Fri May 23 16:37:57 2008 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Fri May 23 16:41:39 2008 +0200
     1.3 @@ -1008,12 +1008,12 @@
     1.4                (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
     1.5            in
     1.6              SOME (gr3, Codegen.mk_app brack
     1.7 -              (Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat
     1.8 -                  (separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
     1.9 -                    [Pretty.block [Pretty.str "val ", pl, Pretty.str " =",
    1.10 +              (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, List.concat
    1.11 +                  (separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
    1.12 +                    [Pretty.block [Codegen.str "val ", pl, Codegen.str " =",
    1.13                         Pretty.brk 1, pr]]) qs))),
    1.14 -                Pretty.brk 1, Pretty.str "in ", pu,
    1.15 -                Pretty.brk 1, Pretty.str "end"])) pargs)
    1.16 +                Pretty.brk 1, Codegen.str "in ", pu,
    1.17 +                Pretty.brk 1, Codegen.str "end"])) pargs)
    1.18            end
    1.19      end
    1.20    | _ => NONE);
    1.21 @@ -1029,8 +1029,8 @@
    1.22                 (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
    1.23             in
    1.24               SOME (gr2, Codegen.mk_app brack
    1.25 -               (Pretty.block [Pretty.str "(fn ", q, Pretty.str " =>",
    1.26 -                 Pretty.brk 1, pu, Pretty.str ")"]) pargs)
    1.27 +               (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
    1.28 +                 Pretty.brk 1, pu, Codegen.str ")"]) pargs)
    1.29             end
    1.30         | _ => NONE)
    1.31    | _ => NONE);