src/Pure/term.ML
changeset 18995 ff4e4773cc7c
parent 18981 a7b7cf408cff
child 19014 f70ced571ba8
     1.1 --- a/src/Pure/term.ML	Fri Feb 10 02:22:32 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Fri Feb 10 02:22:35 2006 +0100
     1.3 @@ -131,10 +131,6 @@
     1.4    val variant: string list -> string -> string
     1.5    val variantlist: string list * string list -> string list
     1.6      (*note reversed order of args wrt. variant!*)
     1.7 -  val add_typ_classes: typ * class list -> class list
     1.8 -  val add_typ_tycons: typ * string list -> string list
     1.9 -  val add_term_classes: term * class list -> class list
    1.10 -  val add_term_tycons: term * string list -> string list
    1.11    val add_term_consts: term * string list -> string list
    1.12    val term_consts: term -> string list
    1.13    val exists_subterm: (term -> bool) -> term -> bool
    1.14 @@ -1089,17 +1085,7 @@
    1.15  
    1.16  (** Consts etc. **)
    1.17  
    1.18 -fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts
    1.19 -  | add_typ_classes (TFree (_, S), cs) = S union cs
    1.20 -  | add_typ_classes (TVar (_, S), cs) = S union cs;
    1.21 -
    1.22 -fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins_string cs) Ts
    1.23 -  | add_typ_tycons (_, cs) = cs;
    1.24 -
    1.25 -val add_term_classes = it_term_types add_typ_classes;
    1.26 -val add_term_tycons = it_term_types add_typ_tycons;
    1.27 -
    1.28 -fun add_term_consts (Const (c, _), cs) = c ins_string cs
    1.29 +fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
    1.30    | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
    1.31    | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
    1.32    | add_term_consts (_, cs) = cs;