src/Pure/term.ML

     -> term -> term option
   val instantiateT_option: ((indexname * sort) * typ) list -> typ -> typ option
   val maxidx_typ: typ -> int -> int
   val maxidx_typs: typ list -> int -> int
   val maxidx_term: term -> int -> int
+  val declare_term_names: term -> Name.context -> Name.context
   val dest_abs: string * typ * term -> string * term
   val zero_var_indexesT: typ -> typ
   val zero_var_indexes: term -> term
   val zero_var_indexes_inst: term ->
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list

   | add_term_names (Free(a,_), bs) = a ins_string bs
   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
   | add_term_names (_, bs) = bs;
 
+fun declare_term_names (Const (a, _)) = Name.declare (NameSpace.base a)
+  | declare_term_names (Free (a, _)) = Name.declare a
+  | declare_term_names (t $ u) = declare_term_names t #> declare_term_names u
+  | declare_term_names (Abs (_, _, t)) = declare_term_names t
+  | declare_term_names _ = I;
+
 (*Accumulates the TVars in a type, suppressing duplicates. *)
 fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
   | add_typ_tvars(TFree(_),vs) = vs
   | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
 

 
 fun term_frees t = add_term_frees(t,[]);
 
 (*Given an abstraction over P, replaces the bound variable by a Free variable
   having a unique name -- SLOW!*)
-fun variant_abs (a,T,P) =
-  let val b = Name.variant (add_term_names(P,[])) a
-  in  (b,  subst_bound (Free(b,T), P))  end;
+fun variant_abs (x, T, b) =
+  let val ([x'], _) = Name.variants [x] (declare_term_names b Name.context)
+  in (x', subst_bound (Free (x', T), b))  end;
 
 fun dest_abs (x, T, body) =
   let
     fun name_clash (Free (y, _)) = (x = y)
       | name_clash (t $ u) = name_clash t orelse name_clash u

       dest_abs (Name.variant [x] x, T, body)    (*potentially slow, but rarely happens*)
     else (x, subst_bound (Free (x, T), body))
   end;
 
 (* renames and reverses the strings in vars away from names *)
-fun rename_aTs names vars : (string*typ)list =
-  let fun rename_aT (vars,(a,T)) =
-                (Name.variant (map #1 vars @ names) a, T) :: vars
-  in Library.foldl rename_aT ([],vars) end;
-
-fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
+fun rename_aTs names vars =
+  rev (fst (Name.variants (map fst vars) names) ~~ map snd vars);
+
+fun rename_wrt_term t = rename_aTs (declare_term_names t Name.context);
 
 
 (* zero var indexes *)
 
 fun zero_var_inst vars =