src/Pure/term.ML

   val mem_term: term * term list -> bool
   val subset_term: term list * term list -> bool
   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
   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   val typ_subst_TVars: (indexname * typ) list -> typ -> typ

 
 fun union_term (xs, []) = xs
   | 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
   | eq_sort ((s::ss), (t::ts)) = s=t andalso eq_sort(ss,ts)
   | eq_sort (_, _) = false;