REMOVE-UNTOUCHABLE

remove name or list of names to the list of untouchable symbols
Major Section:  EVENTS

Examples:
(remove-untouchable my-var nil)
(remove-untouchable set-mem t)

General Form: (remove-untouchable name{s} fn-p :doc doc-string)

where name{s} is a non-nil symbol or a non-nil true list of symbols, fn-p is any value (but generally nil or t), and doc-string is an optional documentation string not beginning with ``:doc-section ...''. If name{s} is a symbol it is treated as the singleton list containing that symbol. The effect of this event is to remove the given symbols from the list of ``untouchable variables'' in the current world if fn-p is nil, else to remove the symbols into the list of ``untouchable functions''. This event is redundant if no symbol listed is a member of the appropriate untouchables list (variables or functions).

Note that remove-untouchable is illegal by default, since it can be used to provide access to ACL2 internal functions and data structures that are intentionally made untouchable for the user. If you want to call it, you must first create an active trust tag; see defttag.

Also See push-untouchable.