aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--printing/ppvernac.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 463654a0d0..8814daf70b 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -348,7 +348,7 @@ module Make
prlist_with_sep pr_semicolon (pr_params pr_c)
*)
- let pr_thm_token k = str (Kindops.string_of_theorem_kind k)
+ let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k)
let pr_syntax_modifier = function
| SetItemLevel (l,NextLevel) ->