# HG changeset patch
# User haftmann
# Date 1127140931 -7200
# Node ID 940713ba9d2b20fbdea39084c126c12b28f6f579
# Parent  d691bf893d9f92a7db38467c464c8787b7e9ac27
added make function

diff -r d691bf893d9f -r 940713ba9d2b src/Pure/General/alist.ML
--- 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;