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