src/Pure/term.ML
changeset 20331 ccdd1592f5ff
parent 20239 620a3f297072
child 20511 c7daff0a3193
     1.1 --- a/src/Pure/term.ML	Thu Aug 03 17:30:38 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Aug 03 17:30:39 2006 +0200
     1.3 @@ -130,7 +130,6 @@
     1.4    val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
     1.5    val add_term_tfrees: term * (string * sort) list -> (string * sort) list
     1.6    val add_term_tfree_names: term * string list -> string list
     1.7 -  val add_term_tvarnames: term * string list -> string list
     1.8    val typ_tfrees: typ -> (string * sort) list
     1.9    val typ_tvars: typ -> (indexname * sort) list
    1.10    val term_tfrees: term -> (string * sort) list
    1.11 @@ -1169,8 +1168,6 @@
    1.12  val add_term_tfrees = it_term_types add_typ_tfrees;
    1.13  val add_term_tfree_names = it_term_types add_typ_tfree_names;
    1.14  
    1.15 -val add_term_tvarnames = it_term_types add_typ_varnames;
    1.16 -
    1.17  (*Non-list versions*)
    1.18  fun typ_tfrees T = add_typ_tfrees(T,[]);
    1.19  fun typ_tvars T = add_typ_tvars(T,[]);