SYMBOL-NAME

the name of a symbol (a string) 
Major Section:  ACL2-BUILT-INS

Completion Axiom (completion-of-symbol-name): 

(equal (symbol-name x)
       (if (symbolp x)
           (symbol-name x)
         ""))

Guard for (symbol-name x): 

(symbolp x)