removed obsolete term set operations;
authorwenzelm
Wed Nov 09 16:26:46 2005 +0100 (2005-11-09)
changeset 181318c3089df74ba
parent 18130 108ed679cf5a
child 18132 0e9c9a18f454
removed obsolete term set operations;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Wed Nov 09 16:26:45 2005 +0100
     1.2 +++ b/src/Pure/term.ML	Wed Nov 09 16:26:46 2005 +0100
     1.3 @@ -101,11 +101,7 @@
     1.4    val ins_ix: indexname * indexname list -> indexname list
     1.5    val mem_ix: indexname * indexname list -> bool
     1.6    val mem_term: term * term list -> bool
     1.7 -  val subset_term: term list * term list -> bool
     1.8 -  val eq_set_term: term list * term list -> bool
     1.9    val ins_term: term * term list -> term list
    1.10 -  val union_term: term list * term list -> term list
    1.11 -  val inter_term: term list * term list -> term list
    1.12    val could_unify: term * term -> bool
    1.13    val subst_free: (term * term) list -> term -> term
    1.14    val xless: (string * int) * indexname -> bool
    1.15 @@ -826,22 +822,8 @@
    1.16  fun mem_term (_, []) = false
    1.17    | mem_term (t, t'::ts) = t aconv t' orelse mem_term (t, ts);
    1.18  
    1.19 -fun subset_term ([], ys) = true
    1.20 -  | subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys);
    1.21 -
    1.22 -fun eq_set_term (xs, ys) =
    1.23 -    xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs));
    1.24 -
    1.25  fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
    1.26  
    1.27 -fun union_term (xs, []) = xs
    1.28 -  | union_term ([], ys) = ys
    1.29 -  | union_term ((x :: xs), ys) = union_term (xs, ins_term (x, ys));
    1.30 -
    1.31 -fun inter_term ([], ys) = []
    1.32 -  | inter_term (x::xs, ys) =
    1.33 -      if mem_term (x,ys) then x :: inter_term(xs,ys) else inter_term(xs,ys);
    1.34 -
    1.35  
    1.36  (*A fast unification filter: true unless the two terms cannot be unified.
    1.37    Terms must be NORMAL.  Treats all Vars as distinct. *)