 
 (defun idris-thing-at-point ()
   "Return the line number and name at point"
-  (let ((name (string-no-properties (symbol-name (symbol-at-point))))
+  (let ((name (symbol-at-point))
         (line (idris-get-line-num)))
-    (cons name line)))
+    (if name
+        (cons (string-no-properties (symbol-name name)) line)
+      (error "Nothing identifiable under point"))))
 
 (defun idris-load ()
   "Load the current buffer using Idris client mode"

  (idris-load)
  (let ((what (idris-thing-at-point)))
   (call-idris-client (concat ":am! " (number-to-string (cdr what)) " " (car what))))
  (revert-buffer t t))

;;;; Bindings to imitate Agda somewhat
(define-key idris-mode-map (kbd "C-c C-c") 'idris-case-split)

(defun idris-type-at-point ()
  "Show the type of the name at point"
  (interactive)
  (message (call-idris-client (concat ":t " (car (idris-thing-at-point))) t)))

(defun idris-add-clause ()
  "Add clauses to the declaration at point"
