# HG changeset patch
# User wenzelm
# Date 976725670 -3600
# Node ID d2a7c5be62be30a4be883de11846dd8d22e10655
# Parent  cd07dd2ccd36bc63baa92e60bd4f0bcce8f42352
fixed add_term_names: NameSpace.base;

diff -r cd07dd2ccd36 -r d2a7c5be62be src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Dec 13 16:22:10 2000 +0100
+++ b/src/Pure/term.ML	Wed Dec 13 17:41:10 2000 +0100
@@ -789,7 +789,7 @@
 
 (*Accumulates the names in the term, suppressing duplicates.
   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
-fun add_term_names (Const(a,_), bs) = a ins_string bs
+fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs
   | 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)