src/Pure/term.ML

   val add_tfree_names: term -> string list -> string list
   val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
   val add_tfrees: term -> (string * sort) list -> (string * sort) list
   val add_free_names: term -> string list -> string list
   val add_frees: term -> (string * typ) list -> (string * typ) list
+  val add_const_names: term -> string list -> string list
+  val add_consts: term -> (string * typ) list -> (string * typ) list
   val hidden_polymorphism: term -> (indexname * sort) list
   val declare_typ_names: typ -> Name.context -> Name.context
   val declare_term_names: term -> Name.context -> Name.context
   val declare_term_frees: term -> Name.context -> Name.context
   val variant_frees: term -> (string * 'a) list -> (string * 'a) list

 val add_tfree_names = fold_types add_tfree_namesT;
 val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
 val add_tfrees = fold_types add_tfreesT;
 val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I);
 val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
+val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
+val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I);
 
 (*extra type variables in a term, not covered by its type*)
 fun hidden_polymorphism t =
   let
     val T = fastype_of t;