--- a/src/HOL/Tools/inductive_codegen.ML Wed Aug 11 15:00:31 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Wed Aug 11 15:17:13 2010 +0200
@@ -830,10 +830,10 @@
str "case Seq.pull (testf p) of", Pretty.brk 1,
str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"],
str " =>", Pretty.brk 1, str "SOME ",
- Pretty.block (str "[" ::
- Pretty.commas (map (fn (s, T) => Pretty.block
- [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args') @
- [str "]"]), Pretty.brk 1,
+ Pretty.enum "," "[" "]"
+ (map (fn (s, T) => Pretty.block
+ [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args'),
+ Pretty.brk 1,
str "| NONE => NONE);"]) ^
"\n\nend;\n";
val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
--- a/src/Pure/Isar/attrib.ML Wed Aug 11 15:00:31 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Wed Aug 11 15:17:13 2010 +0200
@@ -94,8 +94,7 @@
fun pretty_attribs _ [] = []
| pretty_attribs ctxt srcs =
- [Pretty.enclose "[" "]"
- (Pretty.commas (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs))];
+ [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
(* get attributes *)
--- 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;