diff --git a/Makefile b/Makefile
index df019513700d4f72228e3cb4f71018dc7af2b10e..1e925723d4cdc898e6c071d89c41549174e2ac17 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,11 @@
 .PHONY: install
 install:
 	${MAKE} -C encoding install
-	@sed 's:PVSDKPATH:${PWD}:' tools/load-personoj.lisp | cat
+	@echo "Add to ~/.pvs.lisp:"
+	@echo "--------8<----------"
+	cat tools/load-personoj.lisp
+	@echo "(load-personoj)"
+	@echo "--------8<----------"
 
 .PHONY: encoding
 encoding:
diff --git a/encoding/Makefile b/encoding/Makefile
index 662be101673b8ba37faebd7cd9ff0ad3cd56462e..43705c2d558be406c676e2c49d3896ddb0edf397 100644
--- a/encoding/Makefile
+++ b/encoding/Makefile
@@ -1,3 +1,4 @@
+LP = lambdapi
 LP_SRC != find . -type f -name "*.lp"
 
-.include "../lambdapi.mk"
+.include "../mk/lambdapi.mk"
diff --git a/mk/lambdapi.mk b/mk/lambdapi.mk
new file mode 100644
index 0000000000000000000000000000000000000000..6e52f0127f7f0caade6030ed3e2556c5b0b13e2e
--- /dev/null
+++ b/mk/lambdapi.mk
@@ -0,0 +1,25 @@
+# -*- mode: Makefile; tab-width: 4; -*-
+# ex:ts=4 sw=4 filetype=make:
+
+LP_SRC   ?=
+LP_OBJ   ?= ${LP_SRC:S/.lp$/.lpo/}
+LP_FLAGS ?= -v0 -w --gen-obj
+
+all: ${LP_OBJ}
+
+.SUFFIXES: .lp .lpo
+
+.lp.lpo:
+	${LP} check ${LP_FLAGS} ${.IMPSRC}
+
+.PHONY: install
+install: lambdapi.pkg ${LP_SRC} ${LP_OBJ}
+	${LP} install ${LP_SRC} ${LP_OBJ}
+
+.PHONY: uninstall
+uninstall:
+	${LP} uninstall
+
+.PHONY: clean
+clean:
+	find . -name '*.lpo' -exec rm -f {} +
diff --git a/specs/src/dk-sig.lisp b/specs/src/dk-sig.lisp
index b3a037e0359ca72a8221c84325ca59169fb8c029..5c22f425a70ebac3f09f5cec3fabe1dae22adddf 100644
--- a/specs/src/dk-sig.lisp
+++ b/specs/src/dk-sig.lisp
@@ -29,8 +29,8 @@ symbols as they appear in PVS to a list of variants."
 (declaim (ftype (function (symbol list) integer) count-definitions))
 (defun count-definitions (sym sigs)
   "Count the number of definitions of symbol SYM inside signatures SIGS"
-  (flet ((count (sig) (aif (gethash sym (signature-decls sig)) (length it) 0)))
-    (funcall (lrec (lambda (sig f) (+ (count sig) (funcall f))) 0) sigs)))
+  (flet ((count-sig (sig) (aif (gethash sym (signature-decls sig)) (length it) 0)))
+    (funcall (lrec (lambda (sig f) (+ (count-sig sig) (funcall f))) 0) sigs)))
 
 (declaim (ftype (function (integer) string) mksuffix))
 (defun mksuffix (n)
diff --git a/specs/tools/.gitignore b/specs/tools/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..0b5ea42875ac0c7625d0c4c13e851a3d6399d125
--- /dev/null
+++ b/specs/tools/.gitignore
@@ -0,0 +1,3 @@
+*.lp
+*.lpo
+*.lisp
diff --git a/specs/tools/lambdapi.mk b/specs/tools/lambdapi.mk
index ab8efaf577353ac3104ae02efd0db40edc169298..066d9ff09a8aa8324f52f98aa39453ae84841ca2 100644
--- a/specs/tools/lambdapi.mk
+++ b/specs/tools/lambdapi.mk
@@ -1,23 +1,10 @@
 LP       ?= lambdapi
-LP_FLAGS ?= -v0 -w
 LP_SRC   ?=
-LP_OBJ   ?= ${LP_SRC:S/.lp$/.lpo/}
-
-.SUFFIXES: .lpo .lp
 
 all: ${LP_OBJ}
 
-.lp.lpo:
-	${LP} check ${LP_FLAGS} --gen-obj $<
-
-.PHONY: install
-install: lambdapi.pkg ${LP_SR} ${LP_OBJ}
-	${LP} install ${LP_SRC} ${LP_OBJ}
-
-.PHONY: uninstall
-uninstall:
-	${LP} uninstall
-
 .PHONY: clean
 clean:
-	rm -f ${LP_OBJ}
+	rm -rf *.lpo *.lp *.lisp
+
+.include "../../../mk/lambdapi.mk"
diff --git a/specs/tools/prelude/Makefile b/specs/tools/prelude/Makefile
index bc89ebe8eaeba5beda12aa2728c4964587dea12b..2e1b329022d32e9e48da07fd425db36312fd74a6 100644
--- a/specs/tools/prelude/Makefile
+++ b/specs/tools/prelude/Makefile
@@ -1,5 +1,5 @@
 PVS2DK = ../pvs2dk.sh
-LPC    = lambdapi check
+LP     = lambdapi
 
 THEORIES != grep -v -E '^-|\#' theories
 PVSPATH  ?=
diff --git a/tools/lambdapi.mk b/tools/lambdapi.mk
deleted file mode 100644
index f8abb2b2cff5a098bba6d420a8427c22d02f1f4b..0000000000000000000000000000000000000000
--- a/tools/lambdapi.mk
+++ /dev/null
@@ -1,14 +0,0 @@
-#-*- mode: Makefile; tab-width: 4; -*-
-# ex:ts=4 sw=4 filetype=make:
-
-# lambdapi check command
-LPC ?=
-
-.SUFFIXES: .lp .lpo
-
-.lp.lpo:
-	${LPC} -v0 -w --gen-obj ${.IMPSRC}
-
-.PHONY: clean
-clean:
-	rm -rf *.lp *.lpo *.lisp