clarified name context for abstractions -- in contrast to 367e60d9aa1b and Term.variant_frees (*as they are printed :-*);

--- a/src/Pure/proofterm.ML	Wed Aug 14 19:40:30 2019 +0200
+++ b/src/Pure/proofterm.ML	Wed Aug 14 19:50:23 2019 +0200
@@ -1987,12 +1987,7 @@
 
 local
 
-fun declare_names_term (Abs (_, _, b)) = declare_names_term b
-  | declare_names_term (t $ u) = declare_names_term t #> declare_names_term u
-  | declare_names_term (Const (c, _)) = Name.declare (Long_Name.base_name c)
-  | declare_names_term (Free (x, _)) = Name.declare x
-  | declare_names_term _ = I;
-
+val declare_names_term = Term.declare_term_frees;
 val declare_names_term' = fn SOME t => declare_names_term t | NONE => I;
 
 fun declare_names_proof (Abst (_, _, prf)) = declare_names_proof prf