# HG changeset patch
# User wenzelm
# Date 1139534555 -3600
# Node ID ff4e4773cc7ca9878d9e158e2605f71486c17d2c
# Parent  ce724d5bada24219bec27207c76eaa710ae1c8f3
removed obsolete add_typ/term_classes/tycons;

diff -r ce724d5bada2 -r ff4e4773cc7c src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Feb 10 02:22:32 2006 +0100
+++ b/src/Pure/term.ML	Fri Feb 10 02:22:35 2006 +0100
@@ -131,10 +131,6 @@
   val variant: string list -> string -> string
   val variantlist: string list * string list -> string list
     (*note reversed order of args wrt. variant!*)
-  val add_typ_classes: typ * class list -> class list
-  val add_typ_tycons: typ * string list -> string list
-  val add_term_classes: term * class list -> class list
-  val add_term_tycons: term * string list -> string list
   val add_term_consts: term * string list -> string list
   val term_consts: term -> string list
   val exists_subterm: (term -> bool) -> term -> bool
@@ -1089,17 +1085,7 @@
 
 (** Consts etc. **)
 
-fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts
-  | add_typ_classes (TFree (_, S), cs) = S union cs
-  | add_typ_classes (TVar (_, S), cs) = S union cs;
-
-fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins_string cs) Ts
-  | add_typ_tycons (_, cs) = cs;
-
-val add_term_classes = it_term_types add_typ_classes;
-val add_term_tycons = it_term_types add_typ_tycons;
-
-fun add_term_consts (Const (c, _), cs) = c ins_string cs
+fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
   | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
   | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
   | add_term_consts (_, cs) = cs;