--- a/src/Pure/General/alist.ML Mon Sep 19 16:39:27 2005 +0200
+++ b/src/Pure/General/alist.ML Mon Sep 19 16:42:11 2005 +0200
@@ -19,6 +19,7 @@
-> ('b * 'c) list -> ('b * 'c) list
val map_entry: ('a * 'b -> bool) -> 'a -> ('c -> 'c)
-> ('b * 'c) list -> ('b * 'c) list
+ val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
end;
structure AList: ALIST =
@@ -58,4 +59,8 @@
else x :: mapp xs
in if defined eq xs key' then mapp xs else xs end;
+fun make keyfun =
+ let fun keypair x = (x, keyfun x)
+ in map keypair end;
+
end;