# HG changeset patch
# User wenzelm
# Date 1281532633 -7200
# Node ID 16bb1e60204b2b1c76efbd0c1ce94d5f16ce22da
# Parent  36afb56ec49ea1d8a9cace5809f3eb859e81fbf2
use Pretty.enum convenience;

diff -r 36afb56ec49e -r 16bb1e60204b src/HOL/Tools/inductive_codegen.ML
--- 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;
diff -r 36afb56ec49e -r 16bb1e60204b src/Pure/Isar/attrib.ML
--- 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 *)
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;