src/Pure/Isar/attrib.ML
changeset 38329 16bb1e60204b
parent 37198 3af985b10550
child 38330 e98236e5068b
     1.1 --- a/src/Pure/Isar/attrib.ML	Wed Aug 11 15:00:31 2010 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Aug 11 15:17:13 2010 +0200
     1.3 @@ -94,8 +94,7 @@
     1.4  
     1.5  fun pretty_attribs _ [] = []
     1.6    | pretty_attribs ctxt srcs =
     1.7 -      [Pretty.enclose "[" "]"
     1.8 -        (Pretty.commas (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs))];
     1.9 +      [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
    1.10  
    1.11  
    1.12  (* get attributes *)