Constructor macro for honsed constraint-rule-p structures.
(make-honsed-constraint-rule [:thmname <thmname>]
This is identical to make-constraint-rule, except
that we hons the structure we are
This is an ordinary honsing make- macro introduced by
(defmacro make-honsed-constraint-rule (&rest args)
'((:thmname) (:lit-alist) (:syntaxp))