 (defun idris-type-at-point ()
   "Show the type of the name at point"
   (interactive)
-  (message (call-idris-client (concat ":t " (string-no-properties (symbol-name (symbol-at-point)))) t)))
+  (message (call-idris-client (concat ":t " (car (idris-thing-at-point))) t)))
 
 (defun idris-add-clause ()
   "Add clauses to the declaration at point"

(define-key idris-mode-map (kbd "C-c C-t") 'idris-type-at-point)
(define-key idris-mode-map (kbd "C-c C-d") 'idris-add-clause)


(provide 'auto-idris)

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

(defun idris-proof-search (&optional hints)
  "Invoke the proof search"
