added pretty_attribs (from attrib.ML);

--- a/src/Pure/Isar/attrib.ML	Sat Oct 14 23:25:48 2006 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Oct 14 23:25:50 2006 +0200
@@ -18,6 +18,7 @@
   exception ATTRIB_FAIL of (string * Position.T) * exn
   val intern: theory -> xstring -> string
   val intern_src: theory -> src -> src
+  val pretty_attribs: Proof.context -> src list -> Pretty.T list
   val attribute: theory -> src -> attribute
   val attribute_i: theory -> src -> attribute
   val map_specs: ('a -> 'att) ->
@@ -79,11 +80,21 @@
 val print_attributes = AttributesData.print;
 
 
-(* interning *)
+(* name space *)
 
 val intern = NameSpace.intern o #1 o AttributesData.get;
 val intern_src = Args.map_name o intern;
 
+val extern = NameSpace.extern o #1 o AttributesData.get o ProofContext.theory_of;
+
+
+(* pretty printing *)
+
+fun pretty_attribs _ [] = []
+  | pretty_attribs ctxt srcs =
+      [Pretty.enclose "[" "]"
+        (Pretty.commas (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs))];
+
 
 (* get attributes *)