diff --git a/proofs/src/add-hooks.lisp b/proofs/src/add-hooks.lisp
index 7276390d5a93b3a69d86adcfc003bb288e7acfd2..b66fd1be12c512d7d3d1a13f527e7af3f4eb8b84 100644
--- a/proofs/src/add-hooks.lisp
+++ b/proofs/src/add-hooks.lisp
@@ -28,7 +28,7 @@
   (with-slots ((goal current-goal) (ctx context) (crule current-rule)) ps
     (let* ((forms (mapcar #'formula (s-forms goal)))
            (formula (make!-disjunction* forms)))
-      (format stream "Prf ~:/pvs:pp-dk/" formula))))
+      (pvs:pp-dk stream formula))))
 
 (defparameter *ps-counter* 0
   "Number of proofstates encountered. Used to create identifiers.")
@@ -57,7 +57,7 @@
 { \"name\": name of the proposition,
   \"incr\": a unique integer to distinguish the sequents between them,
   \"path\": the path from the root to the current proofstate,
-  \"dk\": the proposition in Dedukti,
+  \"dk\": the proposition in Dedukti (of type Prop),
   \"tac\": some information on the tactic used }"
   (let ((elts
           `((name . ,(prefix-no-dot (label ps)))
diff --git a/proofs/src/proof-dk.lisp b/proofs/src/proof-dk.lisp
deleted file mode 100644
index 1f9737c34f3fe94eb50737c3804c39c1db051c2a..0000000000000000000000000000000000000000
--- a/proofs/src/proof-dk.lisp
+++ /dev/null
@@ -1,9 +0,0 @@
-;; Use `pp-dk' to print the sequent of proof states as Dedukti propositions.
-(in-package :pvs)
-
-(defun ps->dk (ps)
-  "Transform the proofstate PS to a proposition."
-  (with-slots ((goal current-goal) (ctx context) (crule current-rule)) ps
-    (let* ((forms (mapcar #'formula (s-forms goal)))
-           (formula (make!-disjunction* forms)))
-      (format nil "Prf ~:/pvs:pp-dk/" formula))))