 ;;; Subscripts
 
 (defconst fstar-subscripts--font-lock-spec
-  `(,(fstar--fl-conditional-matcher fstar-syntax-id-with-subscript #'fstar--in-code-p)
+  `(,(fstar--fl-conditional-matcher fstar-syntax-id-with-subscript-re #'fstar--in-code-p)
     (1 '(face fstar-subscript-face display (raise -0.3)) append)))
 
 (defun fstar-setup-subscripts ()

  (font-lock-mode -1)
  (setq-local
   font-lock-defaults
   `(((,fstar-syntax-constants    . 'font-lock-constant-face)
      (,fstar-syntax-keywords     . 'font-lock-keyword-face)
      (,fstar-syntax-builtins     . 'font-lock-builtin-face)
      (,fstar-syntax-preprocessor . 'font-lock-preprocessor-face)
      (,fstar-syntax-structure    . 'fstar-structure-face)
      ,@fstar-syntax-additional)
     nil nil))
  (font-lock-set-defaults)

  `(apply-partially #'fstar--re-search-predicated-forward ,cond ,re))

(defconst fstar-syntax-additional
  (let ((id fstar-syntax-id-re))
    `((,fstar-syntax-cs-re
       (0 'font-lock-type-face))
      (,fstar-syntax-universe-re
       (0 'fstar-universe-face))
      (,(fstar--fl-conditional-matcher (concat "`" fstar-syntax-ws-re "+?`") #'fstar--in-code-p)
       (0 'fstar-operator-face append))
      (,(fstar--fl-conditional-matcher "`" #'fstar--in-code-p)
       (0 'font-lock-negation-char-face))
