   `(apply-partially #'fstar--re-search-predicated-forward ,cond ,re))
 
 (defconst fstar-syntax-additional
-  (let ((id fstar-syntax-id))
-    `((,fstar-syntax-cs
+  (let ((id fstar-syntax-id-re))
+    `((,fstar-syntax-cs-re
        (0 'font-lock-type-face))
-      (,fstar-syntax-universe
+      (,fstar-syntax-universe-re
        (0 'fstar-universe-face))
-      (,(fstar--fl-conditional-matcher (concat "`" fstar-syntax-ws "+?`") #'fstar--in-code-p)
+      (,(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))

(defconst fstar-syntax-fsdoc-keywords-re
  (format "^[[:space:]]*\\(%s\\)\\_>" (regexp-opt fstar-syntax-fsdoc-keywords)))

(defconst fstar-syntax-preprocessor-directives
  '("#set-options" "#reset-options" "#light"))

(defconst fstar-syntax-qualifiers

  (format "^\\(?:%s[ \n]\\)*%s "
          (regexp-opt fstar-syntax-qualifiers)
          (regexp-opt (append (remove "and" fstar-syntax-headers)
                              fstar-syntax-preprocessor)))
  "Regexp matching starts of semantic blocks.")

(defconst fstar-syntax-block-delims
  `("begin" "end" "in"))

(defconst fstar-syntax-structure-re
  (regexp-opt (append fstar-syntax-block-delims
                      fstar-syntax-headers
                      fstar-syntax-qualifiers)
              'symbols))

(defconst fstar-syntax-preprocessor-re
  (regexp-opt fstar-syntax-preprocessor 'symbols))

(defconst fstar-syntax-keywords
  '("of"
    "forall" "exists"
    "assert" "assert_norm" "assume"
    "fun" "function"
    "try" "match" "when" "with"
    "if" "then" "else"
    "ALL" "All" "DIV" "Div" "EXN" "Ex" "Exn" "GHOST" "GTot" "Ghost"
    "Lemma" "PURE" "Pure" "Tot" "ST" "STATE" "St"
    "Unsafe" "Stack" "Heap" "StackInline" "Inline"))

(defconst fstar-syntax-keywords-re
  (regexp-opt fstar-syntax-keywords 'symbols))

(defconst fstar-syntax-builtins
  '("requires" "ensures" "modifies" "decreases" "attributes"
    "effect_actions"))

(defconst fstar-syntax-builtins-re
  (regexp-opt fstar-syntax-builtins 'symbols))

(defconst fstar-syntax-ambiguous-re
  (regexp-opt `("\\/" "/\\")))

(defconst fstar-syntax-constants
  '("False" "True"))

(defconst fstar-syntax-constants-re
  (regexp-opt fstar-syntax-constants 'symbols))

(defface fstar-structure-face
  '((((background light)) (:bold t))
