# HG changeset patch # User wenzelm # Date 1131550006 -3600 # Node ID 8c3089df74baef30708c608c313cb4f9741833bb # Parent 108ed679cf5a4e3b38d80d270a8ea3913f85dce7 removed obsolete term set operations; diff -r 108ed679cf5a -r 8c3089df74ba src/Pure/term.ML --- a/src/Pure/term.ML Wed Nov 09 16:26:45 2005 +0100 +++ b/src/Pure/term.ML Wed Nov 09 16:26:46 2005 +0100 @@ -101,11 +101,7 @@ val ins_ix: indexname * indexname list -> indexname list val mem_ix: indexname * indexname list -> bool 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 xless: (string * int) * indexname -> bool @@ -826,22 +822,8 @@ fun mem_term (_, []) = false | mem_term (t, t'::ts) = t aconv t' orelse mem_term (t, ts); -fun subset_term ([], ys) = true - | subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys); - -fun eq_set_term (xs, ys) = - xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs)); - fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; -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); - (*A fast unification filter: true unless the two terms cannot be unified. Terms must be NORMAL. Treats all Vars as distinct. *)