src/Pure/codegen.ML
changeset 38329 16bb1e60204b
parent 37944 4b7afae88c57
child 39253 0c47d615a69b
     1.1 --- a/src/Pure/codegen.ML	Wed Aug 11 15:00:31 2010 +0200
     1.2 +++ b/src/Pure/codegen.ML	Wed Aug 11 15:17:13 2010 +0200
     1.3 @@ -889,9 +889,8 @@
     1.4                mk_app false (str "testf") (map (str o fst) args),
     1.5                Pretty.brk 1, str "then NONE",
     1.6                Pretty.brk 1, str "else ",
     1.7 -              Pretty.block [str "SOME ", Pretty.block (str "[" ::
     1.8 -                Pretty.commas (map (fn (s, _) => str (s ^ "_t ()")) args) @
     1.9 -                  [str "]"])]]),
    1.10 +              Pretty.block [str "SOME ",
    1.11 +                Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]),
    1.12            str ");"]) ^
    1.13        "\n\nend;\n";
    1.14      val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;