diff -r 36afb56ec49e -r 16bb1e60204b src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Aug 11 15:00:31 2010 +0200
+++ b/src/Pure/codegen.ML	Wed Aug 11 15:17:13 2010 +0200
@@ -889,9 +889,8 @@
               mk_app false (str "testf") (map (str o fst) args),
               Pretty.brk 1, str "then NONE",
               Pretty.brk 1, str "else ",
-              Pretty.block [str "SOME ", Pretty.block (str "[" ::
-                Pretty.commas (map (fn (s, _) => str (s ^ "_t ()")) args) @
-                  [str "]"])]]),
+              Pretty.block [str "SOME ",
+                Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]),
           str ");"]) ^
       "\n\nend;\n";
     val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;