diff -r 26535df536ae -r 539319bd6162 src/Pure/General/alist.ML
--- a/src/Pure/General/alist.ML	Tue Sep 20 08:21:49 2005 +0200
+++ b/src/Pure/General/alist.ML	Tue Sep 20 08:23:59 2005 +0200
@@ -20,6 +20,7 @@
   val map_entry: ('a * 'b -> bool) -> 'a -> ('c -> 'c)
     -> ('b * 'c) list -> ('b * 'c) list
   val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
+  val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list
 end;
 
 structure AList: ALIST =
@@ -63,4 +64,10 @@
   let fun keypair x = (x, keyfun x)
   in map keypair end;
 
+fun find eq [] _ = []
+  | find eq ((key, value) :: xs) value' =
+      let
+        val values = find eq xs value'
+      in if eq (value', value) then key :: values else values end;
+
 end;