diff --git a/blueprint/src/preamble/print.tex b/blueprint/src/preamble/print.tex
index e69dcad8b9..a412845404 100644
--- a/blueprint/src/preamble/print.tex
+++ b/blueprint/src/preamble/print.tex
@@ -7,7 +7,14 @@
 \declaretheorem[sibling=theorem]{example}
 
 % Plastex commands
-\newcommand{\uses}[1]{}
 \newcommand{\proves}[1]{}
 \newcommand{\lean}[1]{}
 \newcommand{\leanok}{}
+
+% Make sure that arguments of \uses are real labels, by using invisible refs:
+% latex prints a warning if the label is not defined, but nothing is shown in the pdf file.
+\ExplSyntaxOn
+\NewDocumentCommand{\uses}{m}
+ {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}%
+  \ignorespaces}
+\ExplSyntaxOff