Quoting :doc note-6-4:

  Attempts to submit [congruence] rules had unfortunate consequences in
  the case that the function ``symbol'' is [if] or [quote]: for if,
  rules were appropriately ignored because of the special handling
  that ACL2 already gives to calls of [if] for congruence-based
  reasoning, while for quote, it was possible to get a hard Lisp
  error. Now, attempts to submit such rules will result in a clear
  ACL2 error.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1185 5d84a466-a78b-0930-a311-59b22171a541