# HG changeset patch
# User paulson
# Date 933089425 -7200
# Node ID dd30a72880c77424fbecc82bf2705585593b34e6
# Parent  9bfb8e218b9954c602e104780c9500724acb0a34
added gen_inter

diff -r 9bfb8e218b99 -r dd30a72880c7 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Jul 27 17:19:31 1999 +0200
+++ b/src/Pure/library.ML	Tue Jul 27 17:30:25 1999 +0200
@@ -153,6 +153,7 @@
   val union_int: int list * int list -> int list
   val union_string: string list * string list -> string list
   val gen_union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
+  val gen_inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
   val inter: ''a list * ''a list -> ''a list
   val inter_int: int list * int list -> int list
   val inter_string: string list * string list -> string list
@@ -792,6 +793,12 @@
   | (x :: xs) inter_string ys =
       if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
 
+(*generalized intersection*)
+fun gen_inter eq ([], ys) = []
+  | gen_inter eq (x::xs, ys) = 
+      if gen_mem eq (x,ys) then x :: gen_inter eq (xs, ys)
+	                   else      gen_inter eq (xs, ys);
+
 
 (*subset*)
 fun [] subset ys = true