diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 6b9f147e04d1b375eb23857ca8d50d2f335e331b..ec5d88cd371c3babc33857b51b91a2552d172a02 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -500,9 +500,8 @@ let user_prop_names p =
   | IPDecrease {id_ca=Some ca} -> "@decreases"::code_annot_names ca
   | IPDecrease _ -> [ "@decreases" ]
   | IPLemma {il_name = a; il_pred = l} ->
-      let cat = if l.tp_only_check then "@check" else "@lemma" in
-      let names = cat::a::(ident_names l.tp_statement.pred_name)
-      in begin
+      let names = "@lemma"::a::pred_names l in
+      begin
         match LogicUsage.section_of_lemma a with
         | LogicUsage.Toplevel _ -> names
         | LogicUsage.Axiomatic ax -> ax.LogicUsage.ax_name::names