diff --git a/extras/latex/lstlean.md b/extras/latex/lstlean.md
index fb8dc4340..a2b78b7e1 100644
--- a/extras/latex/lstlean.md
+++ b/extras/latex/lstlean.md
@@ -31,7 +31,6 @@ preamble in your document:
 \definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
 \definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    % blue
 \definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green
-\definecolor{attributecolor}{rgb}{0.7, 0.1, 0.1} % red
 
 \usepackage{listings}
 \def\lstlanguagefiles{lstlean.tex}
diff --git a/extras/latex/lstlean.tex b/extras/latex/lstlean.tex
index 5b14ee8c0..eb7873aad 100644
--- a/extras/latex/lstlean.tex
+++ b/extras/latex/lstlean.tex
@@ -41,15 +41,17 @@ injection, congruence, reflexivity, symmetry, transitivity, state, induction, in
 },
 
 % attributes
-morekeywords=[4]{
-\[persistent\], \[notation\], \[visible\], \[instance\], \[class\], \[parsing-only\],
-\[coercion\], \[unfold-f\], \[constructor\], \[reducible\],
-\[irreducible\], \[semireducible\], \[quasireducible\], \[wf\],
-\[whnf\], \[multiple-instances\], \[none\],
-\[decls\], \[declarations\], \[coercions\], \[classes\],
-\[symm\], \[subst\], \[refl\], \[trans\], \[recursor\],
-\[notations\], \[abbreviations\], \[begin-end-hints\], \[tactic-hints\],
-\[reduce-hints\], \[unfold-hints\], \[aliases\], \[eqv\], \[localrefinfo\]
+% note: 'otherkeywords' is needed because these use a different symbol.
+% this command doesn't allow us to specify a number -- they are put with [1]
+otherkeywords={
+[persistent], [notation], [visible], [instance], [class], [parsing-only],
+[coercion], [unfold-f], [constructor], [reducible],
+[irreducible], [semireducible], [quasireducible], [wf],
+[whnf], [multiple-instances], [none],
+[decls], [declarations], [coercions], [classes],
+[symm], [subst], [refl], [trans], [recursor],
+[notations], [abbreviations], [begin-end-hints], [tactic-hints],
+[reduce-hints], [unfold-hints], [aliases], [eqv], [localrefinfo]
 },
 
 % Various symbols
diff --git a/extras/latex/sample.tex b/extras/latex/sample.tex
index 9d624b456..cbaeb003b 100644
--- a/extras/latex/sample.tex
+++ b/extras/latex/sample.tex
@@ -9,7 +9,6 @@
 \definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
 \definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    % blue
 \definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green
-\definecolor{attributecolor}{rgb}{0.7, 0.1, 0.1} % red
 
 \usepackage{listings}
 \def\lstlanguagefiles{lstlean.tex}