Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed add_term_names: NameSpace.base;
authorwenzelm
Wed, 13 Dec 2000 17:41:10 +0100
changeset 10666 d2a7c5be62be
parent 10665 cd07dd2ccd36
child 10667 75a1c9575edb
fixed add_term_names: NameSpace.base;
src/Pure/term.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle