   (format "^\\(?:%s[ \n]\\)*%s "
           (regexp-opt fstar-syntax-qualifiers)
           (regexp-opt (append (remove "and" fstar-syntax-headers)
-                              fstar-syntax-preprocessor-directives)))
+                              fstar-syntax-preprocessor)))
   "Regexp matching starts of semantic blocks.")
 
-(defconst fstar-syntax-structure
-  (regexp-opt `("begin" "end" "in"
-                ,@fstar-syntax-headers
-                ,@fstar-syntax-qualifiers)
+(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
-  (regexp-opt fstar-syntax-preprocessor-directives 'symbols))
+(defconst fstar-syntax-preprocessor-re
+  (regexp-opt fstar-syntax-preprocessor 'symbols))
 
 (defconst fstar-syntax-keywords
-  (regexp-opt '("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")
-              'symbols))
+  '("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
-  (regexp-opt '("requires" "ensures" "modifies" "decreases" "attributes"
-                "effect_actions")
-              'symbols))
-
-(defconst fstar-syntax-ambiguous
+  '("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-types
-;;   (regexp-opt '("Type")
-;;               'symbols))
-
 (defconst fstar-syntax-constants
-  (regexp-opt '("False" "True")
-              'symbols))
+  '("False" "True"))
+
+(defconst fstar-syntax-constants-re
+  (regexp-opt fstar-syntax-constants 'symbols))
 
 (defface fstar-structure-face
   '((((background light)) (:bold t))

  (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)

      (fstar--find-fun-and-args
       (1 'font-lock-keyword-face)
       (fstar--find-formal (fstar-subexpr-pre-matcher 1) nil (1 'font-lock-variable-name-face append)))
      (,(fstar--fl-conditional-matcher fstar-syntax-ambiguous-re #'fstar--in-code-p)
       (0 'fstar-ambiguous-face append))
      ("!"
       (0 'fstar-dereference-face))
