anchor.diff:      (merge-functions rest (hons-acons name merged-fn master-funcs))))
   
   
  -  (define combine-hints ((user-hint t) (hint smtlink-hint-p))
  +  (define combine-hints ((user-hint smtlink-hint-syntax-p) (hint smtlink-hint-p))
       :returns (combined-hint smtlink-hint-p)
       :ignore-ok t
       :irrelevant-formals-ok t
       (b* ((hint (smtlink-hint-fix hint))
  -         ((unless (smtlink-hint-syntax-p user-hint nil))
  -          (prog2$ (cw "User provided Smtlink hint can't be applied because of
  -    syntax error in the hints: ~q0" user-hint)
  -                  hint))
  -         )
  +         (user-hint (smtlink-hint-syntax-fix user-hint)))
         hint))
   
     (define process-hint ((cl pseudo-term-listp) (user-hint t))
  
positive.code:   :hints (("Goal" :in-theory (enable function-option-syntax-p function-option-name-p
                                       eval-function-option-type function-option-name-lst-p))))
  
  (define function-option-syntax-fix (())
    :returns
    :short "")
  
  (define function-option-lst-syntax-p ((term t) (used function-option-name-lst-p))
    :returns (syntax-good? booleanp)
    :short "Recognizer for function-option-lst-syntax-p."
    (b* (((if (atom term)) (equal term nil))
         ((unless (and (true-listp term) (>= (len term) 2))) nil)
         ((list* first second rest) term)
         ((mv res new-used) (function-option-syntax-p (list first second) used)))
      (and res (function-option-lst-syntax-p rest new-used))))
  
  (define function-option-lst-syntax-fix)
  
  (define function-syntax-p ((term t))
    :returns (syntax-good? booleanp)
  
negative.code:          (hypothesis-lst-syntax-p rest))))
  
  (define hypothesis-lst-syntax-fix ((term hypothesis-lst-syntax-p))
    :returns (fixed-term hypothesis-lst-syntax-p
                         :hints (("Goal"
                                  :in-theory (enable hypothesis-lst-syntax-p))))
    :verify-guards nil
    :short "Fixing function for a hypothesis-lst-syntax-p."
    (mbe :logic (if (consp term)
  