 (defun fstar-find-id (bound)
   (fstar-find-id-maybe-type bound nil))
 
-
-;; (defun fstar-id-with-type-pre-matcher ()
-;;   (or (save-excursion
-;;         (ignore-errors
-;;           (goto-char (match-beginning 0))
-;;           (skip-syntax-backward "-")
-;;           (when (eq (char-before) ?\()
-;;             (up-list)
-;;             (point))))
-;;       (save-excursion
-;;         (condition-case nil
-;;             (forward-sexp)
-;;           (error nil (forward-char)))
-;;         (point))))
-
 (defun fstar-find-fun-and-args (bound)
   (let ((found))
     (while (and (not found) (re-search-forward "\\_<fun\\_>" bound t))

       (fstar-find-id (fstar-subexpr-pre-matcher 2) nil
                      (1 'font-lock-variable-name-face)))
      (fstar-find-id-with-type
       (1 'font-lock-variable-name-face)
       ;; (,id (fstar-id-with-type-pre-matcher) nil (0 'font-lock-type-face))
       )
      (,(concat "\\_<\\(type\\|kind\\)\\( +" id "\\)\\s-*$")
       (1 'fstar-structure-face)
       (2 'font-lock-function-name-face))

                "kind" "type" "logic"
                "private" "opaque" "total" "default"
                "open" "module")
              'symbols))

(defconst fstar-syntax-preprocessor
  (regexp-opt '("#set-options")
              'symbols))

(defconst fstar-syntax-keywords
