--- 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;