# HG changeset patch
# User wenzelm
# Date 1154619039 -7200
# Node ID ccdd1592f5ffa0a52655e731ca76cc2d1c7e51d9
# Parent  6192478fdba527638fca0dbcfbd065f26acba7a8
removed obsolete add_term_tvarnames;

diff -r 6192478fdba5 -r ccdd1592f5ff src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Aug 03 17:30:38 2006 +0200
+++ b/src/Pure/term.ML	Thu Aug 03 17:30:39 2006 +0200
@@ -130,7 +130,6 @@
   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   val add_term_tfree_names: term * string list -> string list
-  val add_term_tvarnames: term * string list -> string list
   val typ_tfrees: typ -> (string * sort) list
   val typ_tvars: typ -> (indexname * sort) list
   val term_tfrees: term -> (string * sort) list
@@ -1169,8 +1168,6 @@
 val add_term_tfrees = it_term_types add_typ_tfrees;
 val add_term_tfree_names = it_term_types add_typ_tfree_names;
 
-val add_term_tvarnames = it_term_types add_typ_varnames;
-
 (*Non-list versions*)
 fun typ_tfrees T = add_typ_tfrees(T,[]);
 fun typ_tvars T = add_typ_tvars(T,[]);