canonical Term.add_var_names;

--- a/src/HOL/Bali/AxExample.thy	Tue Dec 30 21:46:14 2008 +0100
+++ b/src/HOL/Bali/AxExample.thy	Tue Dec 30 21:46:48 2008 +0100
@@ -41,7 +41,7 @@
 
 ML {*
 fun inst1_tac ctxt s t st =
-  case AList.lookup (op =) (rev (Term.add_varnames (Thm.prop_of st) [])) s of
+  case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
   SOME i => instantiate_tac ctxt [((s, i), t)] st | NONE => Seq.empty;
 
 val ax_tac =

--- a/src/HOL/Library/Efficient_Nat.thy	Tue Dec 30 21:46:14 2008 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Dec 30 21:46:48 2008 +0100
@@ -127,7 +127,7 @@
 fun remove_suc thy thms =
   let
     val vname = Name.variant (map fst
-      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
+      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
     val cv = cterm_of 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))))));
@@ -180,7 +180,7 @@
 fun remove_suc_clause thy thms =
   let
     val vname = Name.variant (map fst
-      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
+      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
     fun find_var (t as Const (@{const_name 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;