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