# HG changeset patch
# User wenzelm
# Date 1153855082 -7200
# Node ID 9a19e4de6e2e87e105d002be6341b60df62d2448
# Parent  ae79b9ad722474adea232b9ee5a3aa5fca6f322f
renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);

diff -r ae79b9ad7224 -r 9a19e4de6e2e src/HOL/Library/EfficientNat.thy
--- 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;
diff -r ae79b9ad7224 -r 9a19e4de6e2e src/Pure/Isar/locale.ML
--- 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'));