diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 494b328ce7..6b6d170ca6 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -25,12 +25,11 @@
   "Execute Lean in the current buffer"
   (interactive "sarg: ")
   (let ((target-file-name
-         (lean-get-this-if-true-or-that
-          (buffer-file-name)
-          (flymake-init-create-temp-buffer-copy 'lean-create-temp-in-system-tempdir))))
+         (or (buffer-file-name)
+             (flymake-init-create-temp-buffer-copy 'lean-create-temp-in-system-tempdir))))
     (compile (lean-compile-string
               (lean-get-executable lean-executable-name)
-              (lean-get-this-if-true-or-that arg "")
+              (or arg "")
               target-file-name))))
 
 (defun lean-std-exe ()
diff --git a/src/emacs/lean-util.el b/src/emacs/lean-util.el
index 54530d8006..cb187cf83c 100644
--- a/src/emacs/lean-util.el
+++ b/src/emacs/lean-util.el
@@ -4,13 +4,8 @@
 ;; Author: Soonho Kong
 ;;
 
-(defmacro lean-get-this-if-true-or-that (this that)
-  `(cond (,this ,this)
-         (t ,that)))
-
 (defun lean-get-rootdir ()
-  (lean-get-this-if-true-or-that
-   lean-rootdir
+  (or lean-rootdir
    (error "'lean-rootdir' is not defined. Please have\
 (customize-set-variable 'lean-rootdir \"~/work/lean\")\
 in your emacs configuration.\