src/Pure/General/alist.ML
changeset 18167 4f9410e685df
parent 17911 fbe857bedcd7
child 18453 2b2fbc32550e
--- a/src/Pure/General/alist.ML	Mon Nov 14 15:14:59 2005 +0100
+++ b/src/Pure/General/alist.ML	Mon Nov 14 15:15:07 2005 +0100
@@ -26,6 +26,7 @@
   val merge: ('a * 'a -> bool) -> ('b * 'b -> bool)
     -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list      (*exception DUP*)
   val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list
+  val string_of_alist: ('a -> string) -> ('b -> string) -> ('a * 'b) list -> string
 end;
 
 structure AList: ALIST =
@@ -107,4 +108,9 @@
         val values = find eq xs value';
       in if eq (value', value) then key :: values else values end;
 
+fun string_of_alist string_of_key string_of_value =
+  map (fn (key, value) => string_of_key key ^ " -> " ^ string_of_value value)
+  #> commas
+  #> enclose "[" "]"
+
 end;