# HG changeset patch
# User paulson
# Date 907077583 -7200
# Node ID 8fcb0f181ad6e170c03c9889e392417fe93ee719
# Parent  aad639e56d4eb65bd61b54631060e5d218d7e957
new function inter_term

diff -r aad639e56d4e -r 8fcb0f181ad6 src/Pure/term.ML
--- a/src/Pure/term.ML	Tue Sep 29 15:58:47 1998 +0200
+++ b/src/Pure/term.ML	Tue Sep 29 15:59:43 1998 +0200
@@ -104,6 +104,7 @@
   val eq_set_term: term list * term list -> bool
   val ins_term: term * term list -> term list
   val union_term: term list * term list -> term list
+  val inter_term: term list * term list -> term list
   val could_unify: term * term -> bool
   val subst_free: (term * term) list -> term -> term
   val subst_atomic: (term * term) list -> term -> term
@@ -517,6 +518,10 @@
   | union_term ([], ys) = ys
   | union_term ((x :: xs), ys) = union_term (xs, ins_term (x, ys));
 
+fun inter_term ([], ys) = []
+  | inter_term (x::xs, ys) =
+      if mem_term (x,ys) then x :: inter_term(xs,ys) else inter_term(xs,ys);
+
 (** Equality, membership and insertion of sorts (string lists) **)
 
 fun eq_sort ([]:sort, []) = true