renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);

--- a/src/HOL/Library/EfficientNat.thy	Tue Jul 25 21:18:01 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Tue Jul 25 21:18:02 2006 +0200
@@ -154,7 +154,7 @@
   let
     val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
     val vname = Name.variant (map fst
-      (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
+      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
     val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT));
     fun lhs_of th = snd (Thm.dest_comb
       (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
@@ -207,7 +207,7 @@
   let
     val Suc_clause' = Thm.transfer thy Suc_clause;
     val vname = Name.variant (map fst
-      (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
+      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
     fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
       | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
       | find_var _ = NONE;

--- a/src/Pure/Isar/locale.ML	Tue Jul 25 21:18:01 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Jul 25 21:18:02 2006 +0200
@@ -2090,7 +2090,7 @@
     fun sorts (a, i) = AList.lookup (op =) tvars (a, i);
     val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
     val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
-    val vars' = fold Term.add_term_varnames vs vars;
+    val vars' = fold Term.add_varnames vs vars;
     val _ = if null vars' then ()
          else error ("Illegal schematic variable(s) in instantiation: " ^
            commas_quote (map Syntax.string_of_vname vars'));