                                  (fstar-location-col-from loc)))))
 
 (defun fstar-subp--local-issue-p (issue)
-  "Check if ISSUE came from the current buffer."
-  (-when-let* ((loc (car (fstar-issue-locs issue))))
-    (string= (expand-file-name buffer-file-name)
-             (expand-file-name (fstar-location-filename loc)))))
+  "Check if any location in ISSUE came from the current buffer."
+  ;; Local locations come first in list of locations
+  (fstar-subp--local-loc-p (car (fstar-issue-locs issue))))
 
 (defun fstar-subp-parse-and-highlight-issues (status response overlay)
   "Parse issues in RESPONSE (caused by processing OVERLAY) and display them.

                                :col-to (string-to-number col-to)))
                      :message message)))

(defun fstar-subp-json--parse-location (json)
  "Convert JSON info an fstar-mode location."
  (let-alist json

(defconst fstar-subp-legacy--issue-regexp
  (concat "^" fstar-subp-issue-location-regexp "\\s-*:\\s-*"))

(defconst fstar-subp--also-see-regexp
  (concat " *(\\(?:Also see:\\|see also\\) *" fstar-subp-issue-location-regexp ")"))

(defun fstar-subp-legacy--parse-issue (limit)
  "Construct an issue object from the current match data up to LIMIT."
