           (set-match-data `(,(car md) ,(point) ,@(cddr md))))))
     found))
 
-(defun fstar-find-id (bound)
-  "Find variable name between point and BOUND."
-  (fstar-find-id-maybe-type bound nil))
+(defvar-local fstar--font-lock-anchor nil)
+
+(defun fstar--beginning-of-sexp (pos)
+  "Find beginning of sexp enclosing POS."
+  (or (nth 1 (syntax-ppss pos)) 1))
+
+(defun fstar-subexpr-pre-matcher (rewind-to &optional bound-to)
+  "Move past REWIND-TO th group, then return end of BOUND-TO th.
+This also records the beginning of enclosing sexp in
+`fstar--font-lock-anchor'."
+  (setq-local fstar--font-lock-anchor (fstar--beginning-of-sexp (match-beginning 0)))
+  (goto-char (match-end rewind-to))
+  (match-end (or bound-to 0)))
+
+(defun fstar--directly-under-anchor ()
+  "Check whether point is directly under a binder.
+This works by moving up in the sexp tree and checking that this
+leads to the binder's start."
+  (= (fstar--beginning-of-sexp (point)) (or fstar--font-lock-anchor 1)))
+
+(defun fstar--find-formal (bound)
+  "Find unparenthesized variable name between point and BOUND."
+  (fstar-find-id-maybe-type bound nil #'fstar--directly-under-anchor))
 
 (defun fstar-find-id-with-type (bound)
   "Find var:type pair between point and BOUND."
   (fstar-find-id-maybe-type bound t))
 
-(defun fstar-find-fun-and-args (bound)
-  "Find lambda expression between point and BOUND."
+(defun fstar--search-forward-in-sexp (needle bound)
+  "Find next NEEDLE at current level before BOUND or end of current sexp."
+  (let ((found t) (rejected t)
+        (fstar--font-lock-anchor (fstar--beginning-of-sexp (point))))
+    (save-excursion
+      (while (and found rejected)
+        (setq found (search-forward needle bound t))
+        (setq rejected (and found (not (fstar--directly-under-anchor))))))
+    (when found (goto-char found))))
+
+(defun fstar--find-head-and-args (head tail bound)
+  "Find HEAD .. TAIL expression between point and BOUND."
   (let ((found))
-    (while (and (not found) (re-search-forward "\\_<fun\\_>" bound t))
+    (while (and (not found) (re-search-forward head bound t))
       (-when-let* ((mdata (match-data))
-                   (fnd   (search-forward "->" bound t))) ;;FIXME
-        (set-match-data `(,(car mdata) ,(match-end 0)
-                          ,@mdata))
+                   (fnd (fstar--search-forward-in-sexp tail (min bound (point-at-eol)))))
+        (set-match-data `(,(car mdata) ,(match-end 0) ,@mdata))
         (setq found t)))
     found))
+
+(defun fstar--find-fun-and-args (bound)
+  "Find lambda expression between point and BOUND."
+  (fstar--find-head-and-args "\\_<fun\\_>" "->" bound))
+
+(defun fstar--find-quantifier-and-args (bound)
+  "Find quantified expression between point and BOUND."
+  (fstar--find-head-and-args "\\_<\\(?:forall\\|exists\\)\\_>" "." bound))
 
 (defun fstar-find-subtype-annotation (bound)
   "Find {...} group between point and BOUND."

       (0 'font-lock-type-face))
      (,fstar-syntax-universe
       (1 'fstar-universe-face))
      (,(concat "{\\(:" id "\\) *\\([^}]*\\)}")
       (1 'font-lock-builtin-face append)
       (2 'fstar-attribute-face append))
      (,(concat "\\_<\\(let\\(?: +rec\\)?\\|and\\)\\_>\\(\\(?: +" id "\\)?\\)")
       (1 'fstar-structure-face)
       (2 'font-lock-function-name-face))
      (,(concat "\\_<\\(type\\|kind\\)\\( +" id "\\)")

       (1 'fstar-structure-face)
       (2 'font-lock-function-name-face))
      (fstar-find-id-with-type
       (1 'font-lock-variable-name-face append))
      (fstar-find-subtype-annotation
       (0 'fstar-subtype-face append))
      ("%\\[\\([^]]+\\)\\]"
       (1 'fstar-decreases-face append))
      (fstar--find-quantifier-and-args
       (1 'font-lock-keyword-face)
       (fstar--find-formal (fstar-subexpr-pre-matcher 1) nil (1 'font-lock-variable-name-face append)))
      (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-syntax-ambiguous
       (0 'fstar-ambiguous-face append))
      ("!"
