diff --git a/tools/load-personoj.lisp b/tools/load-personoj.lisp
index 6e91d8460d05ef159a9e1500c47ad0ac6e12102e..b0e571c5b557da20e34e66816099277f7c6b0d38 100644
--- a/tools/load-personoj.lisp
+++ b/tools/load-personoj.lisp
@@ -1,14 +1,11 @@
-;;;; Call (load-personoj) from ~/.pvs.lisp to load Personoj automatically into
-;;;; PVS
-
-(defmacro load-personoj (&optional pth)
+(defun load-personoj (&optional pth)
   "Load Personoj specification exporter and proof exporter. If given, PTH is the
 path to the root of the repository. Otherwise, the root is taken from the
 environment variable PERSONOJ"
   (let ((pth (cond
-               (pth pth)
+               (pth (uiop:ensure-pathname pth))
                ((uiop:getenvp "PERSONOJPATH")
                 (uiop:getenv-pathname "PERSONOJPATH" :ensure-directory t))
                (t (error "Cannot load personoj: PERSONOJPATH not set.")))))
-    `(uiop:with-current-directory (,pth)
-       (load "load.lisp"))))
+    (uiop:with-current-directory (pth)
+      (load "load.lisp"))))
diff --git a/tools/load-pvs.lisp b/tools/load-pvs.lisp
index f8dfe4775a1a36cd5727b6199aed9cf0d85aa28e..483d9b4f4b732d8711470ef3cfc093804e64ddbf 100644
--- a/tools/load-pvs.lisp
+++ b/tools/load-pvs.lisp
@@ -1,15 +1,12 @@
-;;; Place the following definitions into "~/.sbclrc" to be able to load PVS into
-;;; any sbcl session.
-(defmacro load-pvs (&optional pvspath)
+(defun load-pvs (&optional pvspath)
   "Load PVS into the current lisp environment. Argument PVSPATH is the filespec
 to the sources of PVS. If not provided, it is fetched from the environment
 variables PVSPATH."
-  (let (($pvspath (gensym)))
-    `(let ((,$pvspath
-             (cond
-               (,pvspath ,pvspath)
-               ((uiop:getenvp "PVSPATH") (uiop:getenv-pathname "PVSPATH"))
-               (t (error "Cannot load PVS: PVSPATH not set.")))))
-       (uiop:with-current-directory (,$pvspath)
-         (load "pvs.system")
-         (uiop:symbol-call :make "OPERATE-ON-SYSTEM" :pvs :load)))))
+  (let ((pvspath
+          (cond
+            (pvspath (uiop:ensure-pathname pvspath))
+            ((uiop:getenvp "PVSPATH") (uiop:getenv-pathname "PVSPATH"))
+            (t (error "Cannot load PVS: PVSPATH not set.")))))
+    (uiop:with-current-directory (pvspath)
+      (load "pvs.system")
+      (uiop:symbol-call :make "OPERATE-ON-SYSTEM" :pvs :load))))