# HG changeset patch
# User wenzelm
# Date 1565805023 -7200
# Node ID 2d2b5a8e8d59c920dbbc106e83946df17b34cf44
# Parent  81a8eba6639cf71640717107dc6366fe5d3f4e1d
clarified name context for abstractions -- in contrast to 367e60d9aa1b and Term.variant_frees (*as they are printed :-*);

diff -r 81a8eba6639c -r 2d2b5a8e8d59 src/Pure/proofterm.ML
--- 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